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

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := fun n ↦ truncation (X n) ↑n
S : ℕ → Ω → ℝ := fun n ↦ ∑ i ∈ range n, Y i
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := fun n ↦ ⌊c ^ n⌋₊
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * ∫ (a : Ω), X 0 a)
N : ℕ
⊢ ∑ j ∈ range (u (N - 1)), c ^ 5 * (c - 1)⁻¹ ^ 3 / ↑j ^ 2 * Var[Y j; ℙ] =
    c ^ 5 * (c - 1)⁻¹ ^ 3 * ∑ j ∈ range (u (N - 1)), (↑j ^ 2)⁻¹ * Var[Y j; ℙ]

Tactic:
by
        simp_rw [mul_sum, div_eq_mul_inv, mul_assoc]

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Iso

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
M : ModuleCat k[G]
r : k[G]
x : (ofModuleMonoidAlgebra.obj M).ρ.asModule
⊢ counitIsoAddEquiv.toFun (r • x) = (RingHom.id k[G]) r • counitIsoAddEquiv.toFun x

Tactic:
by
        simp [counitIsoAddEquiv]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := fun n ↦ truncation (X n) ↑n
S : ℕ → Ω → ℝ := fun n ↦ ∑ i ∈ range n, Y i
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := fun n ↦ ⌊c ^ n⌋₊
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * ∫ (a : Ω), X 0 a)
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
I3 : ∀ (N : ℕ), ∑ i ∈ range N, ℙ {ω | ↑(u i) * ε ≤ |S (u i) ω - ∫ (a : Ω), S (u i) a|} ≤ ENNReal.ofReal (ε⁻¹ ^ 2 * C)
I4 : ∑' (i : ℕ), ℙ {ω | ↑(u i) * ε ≤ |S (u i) ω - ∫ (a : Ω), S (u i) a|} < ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, ¬↑(u n) * ε ≤ |S (u n) ω - ∫ (a : Ω), S (u n) a|
⊢ ∀ᶠ (n : ℕ) in atTop,
    |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (range ⌊c ^ n⌋₊).sum Y a| < ε * ↑⌊c ^ n⌋₊

Tactic:
simp_rw [S, not_le, mul_comm, Finset.sum_apply] at hω

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := fun n ↦ truncation (X n) ↑n
S : ℕ → Ω → ℝ := fun n ↦ ∑ i ∈ range n, Y i
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := fun n ↦ ⌊c ^ n⌋₊
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * ∫ (a : Ω), X 0 a)
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
I3 : ∀ (N : ℕ), ∑ i ∈ range N, ℙ {ω | ↑(u i) * ε ≤ |S (u i) ω - ∫ (a : Ω), S (u i) a|} ≤ ENNReal.ofReal (ε⁻¹ ^ 2 * C)
I4 : ∑' (i : ℕ), ℙ {ω | ↑(u i) * ε ≤ |S (u i) ω - ∫ (a : Ω), S (u i) a|} < ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, |∑ c ∈ range (u n), Y c ω - ∫ (a : Ω), ∑ c ∈ range (u n), Y c a| < ε * ↑(u n)
⊢ ∀ᶠ (n : ℕ) in atTop,
    |∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (range ⌊c ^ n⌋₊).sum Y a| < ε * ↑⌊c ^ n⌋₊
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep k G
f g : ↑(coind' φ A)
hfg : ∀ (h : H), (Hom.hom f).toLinearMap (MonoidAlgebra.single h 1) = (Hom.hom g).toLinearMap (MonoidAlgebra.single h 1)
⊢ (Hom.hom f).toLinearMap = (Hom.hom g).toLinearMap

Tactic:
ext h

Goal state after:
k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep k G
f g : ↑(coind' φ A)
hfg : ∀ (h : H), (Hom.hom f).toLinearMap (MonoidAlgebra.single h 1) = (Hom.hom g).toLinearMap (MonoidAlgebra.single h 1)
h : H
⊢ ((Hom.hom f).toLinearMap ∘ₗ MonoidAlgebra.lsingle h) 1 = ((Hom.hom g).toLinearMap ∘ₗ MonoidAlgebra.lsingle h) 1
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
⊢ ↑(Nat.card G) = ∑ g, V.character g * V.character g⁻¹

Tactic:
simpa [Nonempty.intro (Iso.refl V), inv_mul_eq_one₀] using char_orthonormal V V

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ Z : Action (Type u) G
f : X✝ ⟶ Y✝
⊢ (linearization k G).obj Z ◁ (linearization k G).map f ≫ ofHom (μ Z Y✝) =
    ofHom (μ Z X✝) ≫ (linearization k G).map (Z ◁ f)

Tactic:
ext1; simp [μ_comp_lTensor _]

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

Goal state before:
pp: case refine_1.succ
k : Type u_1
G : Type u_2
inst✝⁴ : CommRing k
inst✝³ : Group G
V : Type u_4
inst✝² : AddCommGroup V
inst✝¹ : Module k V
ρ : Representation k G V
g : G
inst✝ : Finite G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
α : V
n : ℕ
a✝ : (fun gv ↦ (ρ gv.1) gv.2 - gv.2) ((fun x ↦ g ^ x) n, α) ∈ ↑(ρ g - LinearMap.id).range
⊢ (fun gv ↦ (ρ gv.1) gv.2 - gv.2) ((fun x ↦ g ^ x) (n + 1), α) ∈ ↑(ρ g - LinearMap.id).range

Tactic:
| succ n _ =>

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

Goal state before:
pp: case succ
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
m : ℕ
a✝ : QuasiIsoAt (resolution.π k g) m
⊢ ((HomologicalComplex.sc' ((chainComplexFunctor k g).obj (leftRegular k G)) (m + 2) (m + 1) m).map
      (forget₂ (Rep k G) (ModuleCat k))).Exact

Tactic:
ShortComplex.moduleCat_exact_iff_range_eq_ker

Goal state after:
case succ
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
m : ℕ
a✝ : QuasiIsoAt (resolution.π k g) m
⊢ (ModuleCat.Hom.hom
        ((HomologicalComplex.sc' ((chainComplexFunctor k g).obj (leftRegular k G)) (m + 2) (m + 1) m).map
            (forget₂ (Rep k G) (ModuleCat k))).f).range =
    (ModuleCat.Hom.hom
        ((HomologicalComplex.sc' ((chainComplexFunctor k g).obj (leftRegular k G)) (m + 2) (m + 1) m).map
            (forget₂ (Rep k G) (ModuleCat k))).g).ker
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: case succ
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
n : ℕ
a✝ : ∀ [h₀ : NeZero n], Even n → (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev n) n
h₀ : NeZero (n + 1)
hi : Even (n + 1)
⊢ (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev (n + 1)) (n + 1)

Tactic:
| succ n _ =>

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
h₀ : NeZero i
hi : Even i
⊢ (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev i) i

Tactic:
induction i generalizing h₀ with | zero => exact (NeZero.ne 0 rfl).elim | succ n _ => simp

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

Goal state before:
pp: case h
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
x : L
hx : (Algebra.norm K) x = 1
xu : Lˣ := ⋯
hx' : ↑(toMul (toAdditive ((Hom.hom (ofAlgebraAutOnUnits K L).norm) (toAdditive.symm (ofMul xu))))) = 1
this :
  (CategoryTheory.ConcreteCategory.hom (FiniteCyclicGroup.groupCohomologyπOdd (ofAlgebraAutOnUnits K L) g hg 1 ⋯))
        ⟨toAdditive.symm (ofMul xu), ⋯⟩ =
      0 ↔
    ↑⟨toAdditive.symm (ofMul xu), ⋯⟩ ∈
      (Hom.hom
          ((ofAlgebraAutOnUnits K L).applyAsHom g - CategoryTheory.CategoryStruct.id (ofAlgebraAutOnUnits K L))).range
y : ↑(ofAlgebraAutOnUnits K L)
hy :
  (Hom.hom
          ((ofAlgebraAutOnUnits K L).applyAsHom g -
            CategoryTheory.CategoryStruct.id (ofAlgebraAutOnUnits K L))).toLinearMap
      y =
    ↑⟨toAdditive.symm (ofMul xu), ⋯⟩
⊢ g ↑(toMul (toAdditive y)) / ↑(toMul (toAdditive y)) = x

Tactic:
have := Units.ext_iff.1 congr(toMul <| toAdditive $hy)

Goal state after:
case h
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
x : L
hx : (Algebra.norm K) x = 1
xu : Lˣ := ⋯.unit
hx' : ↑(toMul (toAdditive ((Hom.hom (ofAlgebraAutOnUnits K L).norm) (toAdditive.symm (ofMul xu))))) = 1
this✝ :
  (CategoryTheory.ConcreteCategory.hom (FiniteCyclicGroup.groupCohomologyπOdd (ofAlgebraAutOnUnits K L) g hg 1 ⋯))
        ⟨toAdditive.symm (ofMul xu), ⋯⟩ =
      0 ↔
    ↑⟨toAdditive.symm (ofMul xu), ⋯⟩ ∈
      (Hom.hom
          ((ofAlgebraAutOnUnits K L).applyAsHom g - CategoryTheory.CategoryStruct.id (ofAlgebraAutOnUnits K L))).range
y : ↑(ofAlgebraAutOnUnits K L)
hy :
  (Hom.hom
          ((ofAlgebraAutOnUnits K L).applyAsHom g -
            CategoryTheory.CategoryStruct.id (ofAlgebraAutOnUnits K L))).toLinearMap
      y =
    ↑⟨toAdditive.symm (ofMul xu), ⋯⟩
this :
  ↑(toMul
        (toAdditive
          ((Hom.hom
                ((ofAlgebraAutOnUnits K L).applyAsHom g -
                  CategoryTheory.CategoryStruct.id (ofAlgebraAutOnUnits K L))).toLinearMap
            y))) =
    ↑(toMul (toAdditive ↑⟨toAdditive.symm (ofMul xu), ⋯⟩))
⊢ g ↑(toMul (toAdditive y)) / ↑(toMul (toAdditive y)) = x
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: case refine_2
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)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝¹ : Module.IsTorsionFree A L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
hε : (algebraMap B L) η * ((algebraMap A L) t * g (IsLocalization.mk' L a b)) = t • IsLocalization.mk' L a b
⊢ η * ((galRestrict A K L B) g) a = a

Tactic:
← Algebra.smul_def t,

Goal state after:
case refine_2
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)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝¹ : Module.IsTorsionFree A L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
hε : (algebraMap B L) η * t • g (IsLocalization.mk' L a b) = t • IsLocalization.mk' L a b
⊢ η * ((galRestrict A K L B) g) a = a
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ toCocycles A 1 2 ≫ (isoCocycles₂ A).hom = (cochainsIso₁ A).hom ≫ (shortComplexH2 A).moduleCatLeftHomologyData.f'

Tactic:
by
  simp [← cancel_mono (shortComplexH2 A).moduleCatLeftHomologyData.i, comp_d₁₂_eq,
    shortComplexH2_f]

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

Goal state before:
pp: case succ
k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
n : ℕ
a✝ : ∀ [h₀ : NeZero n], Even n → (ComplexShape.down ℕ).Rel n ((ComplexShape.down ℕ).next n)
h₀ : NeZero (n + 1)
hi : Even (n + 1)
⊢ (ComplexShape.down ℕ).Rel (n + 1) ((ComplexShape.down ℕ).next (n + 1))

Tactic:
| succ n _ =>

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

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
h₀ : NeZero i
hi : Even i
⊢ (ComplexShape.down ℕ).Rel i ((ComplexShape.down ℕ).next i)

Tactic:
induction i generalizing h₀ with | zero => exact (NeZero.ne 0 rfl).elim | succ n _ => simp

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 by_cases u = t * s <;> simp_all

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
p : MvPowerSeries σ R
x : σ →₀ ℕ
⊢ (coeff (embDomain e x)) ((rename ⇑e) p) = (coeff x) p

Tactic:
coeff_rename,

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
p : MvPowerSeries σ R
x : σ →₀ ℕ
⊢ ∑ x ∈ ⋯.toFinset, (coeff x) p = (coeff x) p
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : CommSemiring R
p : MvPowerSeries σ R
⊢ (coeff 0) ((rename f) p) = (coeff 0) p

Tactic:
coeff_rename,

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : CommSemiring R
p : MvPowerSeries σ R
⊢ ∑ x ∈ ⋯.toFinset, (coeff x) p = (coeff 0) p
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✝¹ : Fin 1 → G
x✝ : ↑A
⊢ (ModuleCat.Hom.hom ((chainsIso₁ A).hom ≫ d₁₀ A)) (single x✝¹ x✝) =
    (ModuleCat.Hom.hom ((inhomogeneousChains A).d 1 0 ≫ (chainsIso₀ A).hom)) (single x✝¹ x✝)

Tactic:
simp [chainsIso₀, chainsIso₁, d₁₀_single (G := G), ChainComplex.of.d,
      Unique.eq_default (α := Fin 0 → G), sub_eq_add_neg, inhomogeneousChains.d_single (G := G)]

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 : G →₀ ↑A
⊢ x ∈ cycles₁ A ↔ (x.sum fun g a ↦ (A.ρ g⁻¹) a) = x.sum fun x a ↦ a

Tactic:
by
  change x.sum (fun g a => A.ρ g⁻¹ a - a) = 0 ↔ _
  rw [sum_sub, sub_eq_zero]

Goal state after:
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 : τ →₀ ℕ
⊢ (coeff n) ((rename f) p) = (coeff n) (subst (X ∘ f) p)

Tactic:
coeff_rename,

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 = (coeff n) (subst (X ∘ f) p)
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 : ↑(shortComplexH0 A).X₂
hx : (Coinvariants.mk A.ρ) x = 0
⊢ ∃ x₁, (ConcreteCategory.hom (shortComplexH0 A).f) x₁ = x

Tactic:
Coinvariants.mk_eq_zero,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑(shortComplexH0 A).X₂
hx : x ∈ Coinvariants.ker A.ρ
⊢ ∃ x₁, (ConcreteCategory.hom (shortComplexH0 A).f) x₁ = x
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (t : Set R), t ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(I ^ i) ⊆ t

Tactic:
intro U
    rw [I.ringFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff]
    constructor
    · rintro ⟨-, ⟨i, rfl⟩, h⟩
      replace h : ↑(I ^ i) ⊆ U := by simpa using h
      exact ⟨i, trivial, h⟩
    · rintro ⟨i, -, h⟩
      exact ⟨(I ^ i : Ideal R), ⟨i, by simp⟩, h⟩

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

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
I : Ideal R⟦X⟧
S : Set R
P✝ : Ideal R⟦X⟧
inst✝² : P✝.IsPrime
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsDomain R
P : Ideal R⟦X⟧
h₁ : P ≠ ⊥
h₂ : P.IsPrime
hXP : X ∉ P
⊢ ∃ x ∈ P, Prime x

Tactic:
· obtain ⟨_, h⟩ := (IsPrincipalIdealRing.principal (P.map constantCoeff)).principal
    obtain ⟨_, rfl, _, h⟩ := exist_eq_span_eq_ncard_of_X_notMem hXP h.symm (finite_singleton _)
    simp only [ncard_singleton, ncard_eq_one] at h
    obtain ⟨_, rfl⟩ := h
    exact ⟨_, mem_span_singleton_self _,
      (span_singleton_prime (span_singleton_eq_bot.not.1 h₁)).1 h₂⟩

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : ¬optionElim n y = x
h3 : n = x none
h : y = x.some
u : Option σ
⊢ (optionElim n y) u = x u

Tactic:
cases u <;> simp_all

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

Goal state before:
pp: case succ
S : Type u_3
inst✝¹ : CommRing S
inst✝ : IsNoetherianRing S
n : ℕ
a✝ : IsNoetherianRing (MvPowerSeries (Fin n) S)
⊢ IsNoetherianRing (MvPowerSeries (Fin (n + 1)) S)

Tactic:
| succ n _ =>

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
i : σ
⊢ (MvPowerSeries.rename fun x ↦ i) X = MvPowerSeries.X i

Tactic:
X_apply,

Goal state after:
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
i : σ
⊢ (MvPowerSeries.rename fun x ↦ i) (MvPowerSeries.X ()) = MvPowerSeries.X i
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
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
⊢ Epi (map (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv 1)

Tactic:
convert! epi_of_epi (H1π A) _
  rw [H1π_comp_map]
  exact @epi_comp _ _ _ _ _ _ (mapCycles₁_quotientGroupMk'_epi A S) (H1π _) inferInstance

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
φ : A ⟶ res f B
n : ℕ
S : Subgroup G
inst✝ : S.Normal
⊢ Epi (H1CoresCoinf A S).g

Tactic:
rw [ModuleCat.epi_iff_surjective]
  intro x
  induction x using H1_induction_on with | @h x =>
/- Let `x : Z₁(G ⧸ S, A_S)`. We know `Z₁(G, A_S) ⟶ Z₁(G ⧸ S, A_S)` is surjective, so pick
`y : Z₁(G, A_S)` in the preimage of `x`. -/
  rcases (ModuleCat.epi_iff_surjective _).1
    (mapCycles₁_quotientGroupMk'_epi (A.toCoinvariants S) S) x with ⟨y, hy⟩
/- We know `C₁(G, A) ⟶ C₁(G, A_S)` is surjective, so pick `Y` in the preimage of `y`. -/
  rcases mapRange_surjective _ (map_zero _)
    (Coinvariants.mk_surjective (A.ρ.comp S.subtype)) y.1 with ⟨Y, hY⟩
/- Then `d(Y) ∈ I(S)A,` since `d(y) = 0`. -/
  have : d₁₀ _ Y ∈ Coinvariants.ker (A.ρ.comp S.subtype) := by
    have h' := congr($((mapShortComplexH1 (B := toCoinvariants A S)
      (MonoidHom.id G) (toCoinvariantsMkQ A S)).comm₂₃) Y)
    simp_all [shortComplexH1, ← Coinvariants.mk_eq_zero]
  /- Thus we can pick a representation of `d(Y)` as a sum `∑ ρ(sᵢ⁻¹)(aᵢ) - aᵢ`, `sᵢ ∈ S, aᵢ ∈ A`,
and `Y - ∑ aᵢ·sᵢ` is a cycle. -/
  rcases chains₁ToCoinvariantsKer_surjective
    (res S.subtype A) ⟨d₁₀ A Y, this⟩ with ⟨(Z : S →₀ A), hZ⟩
  have H : d₁₀ A (Y - mapDomain S.subtype Z) = 0 := by
    simpa [map_sub, sub_eq_zero, chains₁ToCoinvariantsKer, -LinearMap.sub_apply, d₁₀,
      sum_mapDomain_index_inj] using! Subtype.ext_iff.1 hZ.symm
  use H1π A ⟨Y - mapDomain S.subtype Z, H⟩
  simp only [H1CoresCoinf_X₃, H1CoresCoinf_X₂, H1CoresCoinf_g,
    Subgroup.coe_subtype, H1π_comp_map_apply]
/- Moreover, the image of `Y - ∑ aᵢ·sᵢ` in `Z₁(G ⧸ S, A_S)` is `x - ∑ aᵢ·1`, and hence differs from
`x` by a boundary, since `aᵢ·1 = d(aᵢ·(1, 1))`. -/
  refine (H1π_eq_iff _ _).2 ?_
  simpa [← hy, mapCycles₁_hom, map_sub, Rep.hom_id (res _ _), ← mapDomain_comp,
    ← mapDomain_mapRange, hY, Function.comp_def, (QuotientGroup.eq_one_iff <| Subtype.val _).2
    (Subtype.prop _)] using! Submodule.finsuppSum_mem _ _ _ _ fun _ _ ↦ single_one_mem_boundaries₁ _

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  (↑(Algebra.TensorProduct.comm R (SymmetricAlgebra R M) (SymmetricAlgebra R M))).comp
      (Bialgebra.comulAlgHom R (SymmetricAlgebra R M)) =
    Bialgebra.comulAlgHom R (SymmetricAlgebra R M)
⊢ ↑(TensorProduct.comm R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul

Tactic:
exact congr(($h).toLinearMap)

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
x✝ : Aᵐᵒᵖ
⊢ (TensorProduct.assoc R Aᵐᵒᵖ Aᵐᵒᵖ Aᵐᵒᵖ)
      ((map (map ↑(opLinearEquiv R) ↑(opLinearEquiv R)) LinearMap.id)
        ((map comul LinearMap.id)
          ((map (↑(opLinearEquiv R).symm) LinearMap.id)
            ((map ↑(opLinearEquiv R) ↑(opLinearEquiv R)) (comul ((opLinearEquiv R).symm x✝)))))) =
    (map (↑(opLinearEquiv R))
        ((map ↑(opLinearEquiv R) ↑(opLinearEquiv R) ∘ₗ comul ∘ₗ ↑(opLinearEquiv R).symm) ∘ₗ ↑(opLinearEquiv R)))
      (comul ((opLinearEquiv R).symm x✝))

Tactic:
simp_rw [← map_map_assoc, map_map, comp_assoc, ← lTensor_comp_rTensor]

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
x✝ : Aᵐᵒᵖ
⊢ (lTensor Aᵐᵒᵖ (lTensor Aᵐᵒᵖ LinearMap.id ∘ₗ rTensor Aᵐᵒᵖ ↑(opLinearEquiv R)) ∘ₗ
        rTensor (A ⊗[R] Aᵐᵒᵖ) ↑(opLinearEquiv R))
      ((TensorProduct.assoc R A A Aᵐᵒᵖ)
        ((lTensor (A ⊗[R] A) (LinearMap.id ∘ₗ LinearMap.id ∘ₗ ↑(opLinearEquiv R)) ∘ₗ
            rTensor A (comul ∘ₗ ↑(opLinearEquiv R).symm ∘ₗ ↑(opLinearEquiv R)))
          (comul ((opLinearEquiv R).symm x✝)))) =
    (lTensor Aᵐᵒᵖ
          ((lTensor Aᵐᵒᵖ ↑(opLinearEquiv R) ∘ₗ rTensor A ↑(opLinearEquiv R)) ∘ₗ
            comul ∘ₗ ↑(opLinearEquiv R).symm ∘ₗ ↑(opLinearEquiv R)) ∘ₗ
        rTensor A ↑(opLinearEquiv R))
      (comul ((opLinearEquiv R).symm x✝))