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

Goal state before:
pp: case refine_2
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
hX : Measurable X
h : HasSubgaussianMGF X c κ ν
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * id ω)) (⇑(κ.map X) ∘ₘ ν)

pp: case refine_3
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
hX : Measurable X
h : HasSubgaussianMGF X c κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf id ((κ.map X) ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
· rw [← Kernel.deterministic_comp_eq_map hX, ← Measure.comp_assoc,
      Measure.deterministic_comp_eq_map, integrable_map_measure (by fun_prop) hX.aemeasurable]
    exact h.integrable_exp_mul t

Goal state after:
case refine_3
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
hX : Measurable X
h : HasSubgaussianMGF X c κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf id ((κ.map X) ω') t ≤ rexp (↑c * t ^ 2 / 2)
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
N : Submodule A[G] M
g : G
v : RestrictScalars A A[G] M
hv : v ∈ { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }
⊢ ((Representation.ofModule M) g) v ∈ { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }

Tactic:
by
    simpa [Representation.ofModule, RestrictScalars.lsmul] using!
      Submodule.smul_of_tower_mem N (MonoidAlgebra.single g 1) hv

Goal state after:
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
N : Submodule A[G] ρ.asModule
g : G
w : W
hw : w ∈ { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }
x✝ : Module A[G] W := ρ.instModuleMonoidAlgebraAsModule
h : 1 • (ρ g) (ρ.asModuleEquiv w) ∈ N
⊢ (ρ g) w ∈ { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }

Tactic:
one_smul

Goal state after:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
N : Submodule A[G] ρ.asModule
g : G
w : W
hw : w ∈ { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }
x✝ : Module A[G] W := ρ.instModuleMonoidAlgebraAsModule
h : (ρ g) (ρ.asModuleEquiv w) ∈ N
⊢ (ρ g) w ∈ { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case hg
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
p : ℝ≥0 := ⋯
q : ℝ≥0 := ⋯
ω' : Ω'
hmX : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑cX * t ^ 2 / 2)
hmY : ∀ (t : ℝ), mgf Y (κ ω') t ≤ rexp (↑cY * t ^ 2 / 2)
hlX : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω')
hlY : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * Y ω)) (↑q) (κ ω')
t : ℝ
⊢ MemLp (fun a ↦ rexp (t * Y a)) (ENNReal.ofReal ↑q) (κ ω')

Tactic:
· simpa using (hlY t)

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ -A ≤ A

Tactic:
linarith

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
this : ∀ᵐ (x : ℝ) ∂Measure.map f μ, 0 ≤ x
x : ℝ
hx : 0 ≤ x
a✝ : A < x
h''x : x ≤ 0
⊢ x = 0

Tactic:
linarith

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
c : ι → ℝ≥0
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
this : IsProbabilityMeasure μ
⊢ HasSubgaussianMGF (fun ω ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert i s his h =>
    simp_rw [← Finset.sum_apply, Finset.sum_insert his, Pi.add_apply, Finset.sum_apply]
    have h_indep' := (h_indep.indepFun_finsetSum_of_notMem₀ h_meas his).symm
    refine add_of_indepFun (h_subG _ (Finset.mem_insert_self _ _)) (h ?_) ?_
    · exact fun i hi ↦ h_subG _ (Finset.mem_insert_of_mem hi)
    · convert! h_indep'
      rw [Finset.sum_apply]

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : AddCommMonoid W
inst✝¹ : Module A V
inst✝ : Module A W
ρ : Representation A G V
σ : Representation A G W
g : G
φ : ρ.Equiv σ
w : W
this : (ρ g) (φ.symm w) = φ.symm ((σ g) w)
⊢ φ ((ρ g) (φ.symm w)) = (σ g) w

Tactic:
simp [this]

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
H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊
ω : Ω
hω : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
h'ω : (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n
⊢ (fun x ↦ (∑ i ∈ range ⌊c ^ x⌋₊, X i ω) / ↑⌊c ^ x⌋₊ - ∫ (a : Ω), X 0 a) =o[atTop] fun _x ↦ 1

Tactic:
have L : (fun n : ℕ => ∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ⌊c ^ n⌋₊ * 𝔼[X 0]) =o[atTop] fun n =>
      (⌊c ^ n⌋₊ : ℝ) := by
    have A : Tendsto (fun n : ℕ => ⌊c ^ n⌋₊) atTop atTop :=
      tendsto_nat_floor_atTop.comp (tendsto_pow_atTop_atTop_of_one_lt c_one)
    convert! hω.sub (h'ω.comp_tendsto A) using 1
    ext1 n
    simp only [Function.comp_apply, sub_sub_sub_cancel_left]

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
H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊
ω : Ω
hω : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
h'ω : (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n
L : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
⊢ (fun x ↦ (∑ i ∈ range ⌊c ^ x⌋₊, X i ω) / ↑⌊c ^ x⌋₊ - ∫ (a : Ω), X 0 a) =o[atTop] fun _x ↦ 1
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V : FDRep k G
⊢ (↑(Nat.card G))⁻¹ * ∑ g, V.character g = ↑(finrank k ↥(invariants V.ρ))

Tactic:
have : Invertible (Fintype.card G : k) := by
    rwa [Fintype.card_eq_nat_card]
  rw [← (isProj_averageMap V.ρ).trace]
  simp [character, GroupAlgebra.average, _root_.map_sum]

Goal state after:
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 < ε
⊢ ε / 4 + ε / 4 + ε / 4 < ε

Tactic:
linarith

Goal state after:
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝⁹ : CommRing k
G : Type u_2
inst✝⁸ : Group G
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module k[G] V
inst✝⁴ : IsScalarTower k k[G] V
W : Type u_4
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module k[G] W
inst✝ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
h : ∀ (v : V), π (i v) = v
g : G
v : V
⊢ 1 • v = v

Tactic:
one_smul

Goal state after:
k : Type u_1
inst✝⁹ : CommRing k
G : Type u_2
inst✝⁸ : Group G
V : Type u_3
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module k[G] V
inst✝⁴ : IsScalarTower k k[G] V
W : Type u_4
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module k[G] W
inst✝ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
h : ∀ (v : V), π (i v) = v
g : G
v : V
⊢ v = v
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : CommRing k
G : Type u_2
inst✝⁹ : Group G
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module k[G] V
inst✝⁵ : IsScalarTower k k[G] V
W : Type u_4
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module k[G] W
inst✝¹ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
inst✝ : Fintype G
hcard : IsUnit ↑(Nat.card G)
h : ∀ (v : V), π (i v) = v
v : V
⊢ 1 • v = v

Tactic:
one_smul

Goal state after:
k : Type u_1
inst✝¹⁰ : CommRing k
G : Type u_2
inst✝⁹ : Group G
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module k[G] V
inst✝⁵ : IsScalarTower k k[G] V
W : Type u_4
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module k[G] W
inst✝¹ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
inst✝ : Fintype G
hcard : IsUnit ↑(Nat.card G)
h : ∀ (v : V), π (i v) = v
v : V
⊢ v = v
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
X Y : Rep k G
f : X ⟶ Y
g : G
x✝¹ : ↑A →ₗ[k] ↑X
x✝ : ↑A
⊢ (((LinearMap.llcomp k ↑A ↑X ↑Y) (Hom.hom f).toLinearMap ∘ₗ (A.ρ.linHom X.ρ) g) x✝¹) x✝ =
    (((A.ρ.linHom Y.ρ) g ∘ₗ (LinearMap.llcomp k ↑A ↑X ↑Y) (Hom.hom f).toLinearMap) x✝¹) x✝

Tactic:
simp [Representation.IntertwiningMap.toLinearMap_apply, ← hom_comm_apply]

Goal state after:
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
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))

Tactic:
simp [this]

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

Goal state before:
pp: k : Type u
G H K : Type v
inst✝¹⁰ : Ring k
inst✝⁹ : TopologicalSpace k
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalGroup H
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : IsTopologicalGroup K
X : TopRep k G
Y : TopRep k H
Z : TopRep k K
φ : H →ₜ* G
ψ : K →ₜ* H
f : res (↑φ) X ⟶ Y
g : res (↑ψ) Y ⟶ Z
n : ℕ
⊢ cocyclesMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) n = cocyclesMap φ f n ≫ cocyclesMap ψ g n

Tactic:
simp [cocyclesMap, ← HomologicalComplex.cyclesMap_comp, ← cochainsMap_comp]

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

Goal state before:
pp: k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k K
B : Rep k H
C : Rep k G
f : H →* K
g : G →* H
φ : res f A ⟶ B
ψ : res g B ⟶ C
n : ℕ
⊢ cocyclesMap (f.comp g) ((resFunctor g).map φ ≫ ψ) n = cocyclesMap f φ n ≫ cocyclesMap g ψ n

Tactic:
simp [cocyclesMap, ← HomologicalComplex.cyclesMap_comp, ← cochainsMap_comp]

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

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n✝ : ℕ
e : G ≃* H
e' : ↑B ≃ₗ[k] ↑A
he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e'
n : ℕ
g : G
⊢ (MonoidHom.comp A.ρ ↑e) g = ↑e' ∘ₗ B.ρ g ∘ₗ ↑e'.symm

Tactic:
← LinearMap.comp_assoc

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✝ : ℕ
e : G ≃* H
e' : ↑B ≃ₗ[k] ↑A
he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e'
n : ℕ
g : G
⊢ (MonoidHom.comp A.ρ ↑e) g = (↑e' ∘ₗ B.ρ g) ∘ₗ ↑e'.symm
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
z : ↥(cycles₂ X.X₃)
y : G × G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : G →₀ ↑X.X₁
hx : (mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x = (ConcreteCategory.hom (d₂₁ X.X₂)) y
x✝ : Fin 1 → G
⊢ ((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) ((ConcreteCategory.hom (chainsIso₁ X.X₁).inv) x)) x✝ =
    ((ConcreteCategory.hom ((inhomogeneousChains X.X₂).d 2 1)) ((ConcreteCategory.hom (chainsIso₂ X.X₂).inv) y)) x✝

Tactic:
by
    conv_rhs => rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₂₁_comp_inv]
    simp [← hx, chainsIso₁]

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 : σ ↪ τ
t : τ
h : single t 1 ∉ Set.range (embDomain e)
⊢ (killCompl e) (X t) = 0

Tactic:
simpa using! killCompl_monomial_eq_zero (1 : R) h

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
S : Set R
hXI : X ∈ I
hSI : span S = Ideal.map constantCoeff I
⊢ I = span {X} ⊔ Ideal.map C (Ideal.map constantCoeff I)

Tactic:
Ideal.map_map

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
S : Set R
hXI : X ∈ I
hSI : span S = Ideal.map constantCoeff I
⊢ I = span {X} ⊔ Ideal.map (C.comp constantCoeff) I
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hXI : X ∉ I
n : ℕ
F : Fin n → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' : Ideal.map constantCoeff I = span (Set.range (⇑constantCoeff ∘ F))
T : R⟦X⟧ → Fin n → R
hT : ∀ g ∈ I, ∑ i, T g i * (⇑constantCoeff ∘ F) i = constantCoeff g
⊢ I ≤ Submodule.span R⟦X⟧ (Set.range F)

Tactic:
dsimp at hT

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hXI : X ∉ I
n : ℕ
F : Fin n → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' : Ideal.map constantCoeff I = span (Set.range (⇑constantCoeff ∘ F))
T : R⟦X⟧ → Fin n → R
hT : ∀ g ∈ I, ∑ i, T g i * constantCoeff (F i) = constantCoeff g
⊢ I ≤ Submodule.span R⟦X⟧ (Set.range F)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case neg
R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
h1 : x = 0 ∧ k = 1
h2 : ¬k = 1
⊢ 1 = (coeff x) 0

Tactic:
tauto

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(x = 0 ∧ k = 1)
h3 : k = 1
⊢ ¬x = 0

Tactic:
tauto

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

Goal state before:
pp: case neg
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
j : Fin n
k : ℕ
x : Fin n →₀ ℕ
h1 : x = single j 1 ∧ k = 0
h2 : ¬k = 0
⊢ 1 = (coeff x) 0

Tactic:
tauto

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
j : Fin n
k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(x = single j 1 ∧ k = 0)
h3 : k = 0
⊢ ¬x = single j 1

Tactic:
tauto

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

Goal state before:
pp: case neg
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
k : ℕ
x : Fin n →₀ ℕ
h1 : k = 0 ∧ x = 0
h2 : ¬k = 0
⊢ r = (coeff x) 0

Tactic:
tauto

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

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(k = 0 ∧ x = 0)
h3 : k = 0
⊢ ¬x = 0

Tactic:
tauto

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✝ : ℕ
e : G ≃* H
e' : ↑A ≃ₗ[k] ↑B
he : ∀ (g : G), ↑e' ∘ₗ A.ρ g = B.ρ (e g) ∘ₗ ↑e'
n : ℕ
h : H
⊢ B.ρ h = ↑e' ∘ₗ (MonoidHom.comp A.ρ ↑e.symm) h ∘ₗ ↑e'.symm

Tactic:
← LinearMap.comp_assoc

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✝ : ℕ
e : G ≃* H
e' : ↑A ≃ₗ[k] ↑B
he : ∀ (g : G), ↑e' ∘ₗ A.ρ g = B.ρ (e g) ∘ₗ ↑e'
n : ℕ
h : H
⊢ B.ρ h = (↑e' ∘ₗ (MonoidHom.comp A.ρ ↑e.symm) h) ∘ₗ ↑e'.symm
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)
x : G ⧸ S →₀ ↑(A.ofQuotient S)
hx : x ∈ cycles₁ (A.ofQuotient S)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), ↑(s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
a✝ : G ⧸ S
b : a✝ ∈ x.support
a : G
⊢ (A.ρ (s ↑a)⁻¹) (x ↑a) = ((A.ρ.ofQuotient S) (↑a)⁻¹) (x ↑a)

Tactic:
by
      simp [← QuotientGroup.mk_inv, apply_eq_of_coe_eq A.ρ S (s a)⁻¹ a⁻¹ (by simp [hs])]

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

Goal state before:
pp: F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid A
inst✝⁶ : AddCommMonoid B
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
inst✝³ : Module R B
inst✝² : Coalgebra R B
a : A
inst✝¹ : FunLike F A B
inst✝ : CoalgHomClass F R A B
f : F
ha : IsGroupLikeElem R a
⊢ counit (f a) = 1

Tactic:
by rw [CoalgHomClass.counit_comp_apply, ha.counit_eq_one]

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

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R), ∑ x ∈ s ×ˢ s, f x • x.1 ⊗ₜ[R] x.2 = ∑ x ∈ s ×ˢ s, g x • x.1 ⊗ₜ[R] x.2 → ∀ i ∈ s ×ˢ s, f i = g i
⊢ ∑ x ∈ s, x ⊗ₜ[R] ∑ x_1 ∈ s, c x • c x_1 • x_1 = ∑ x ∈ s, ∑ y ∈ s, (c x * c y) • x ⊗ₜ[R] y

Tactic:
tmul_sum,

Goal state after:
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R), ∑ x ∈ s ×ˢ s, f x • x.1 ⊗ₜ[R] x.2 = ∑ x ∈ s ×ˢ s, g x • x.1 ⊗ₜ[R] x.2 → ∀ i ∈ s ×ˢ s, f i = g i
⊢ ∑ x ∈ s, ∑ a ∈ s, x ⊗ₜ[R] (c x • c a • a) = ∑ x ∈ s, ∑ y ∈ s, (c x * c y) • x ⊗ₜ[R] y
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: case h
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
a✝ : p.contentIdeal ≠ ⊤
⊢ ¬IsUnit (Submodule.IsPrincipal.generator p.contentIdeal)

Tactic:
simp_all [← Ideal.span_singleton_eq_top]

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

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
x✝ : K
⊢ x✝ ∈ Set.univ.integer K ↔ x✝ ∈ ⊤

Tactic:
tauto

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

Goal state before:
pp: case refine_1
k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
⊢ (mapShortComplexH2 (g.comp f) (φ ≫ (resFunctor f).map ψ)).τ₁ = (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₁

pp: case refine_2
k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
⊢ (mapShortComplexH2 (g.comp f) (φ ≫ (resFunctor f).map ψ)).τ₂ = (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₂

pp: case refine_3
k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
⊢ (mapShortComplexH2 (g.comp f) (φ ≫ (resFunctor f).map ψ)).τ₃ = (mapShortComplexH2 f φ ≫ mapShortComplexH2 g ψ).τ₃

Tactic:
all_goals
  { simp only [shortComplexH2]
    ext
    simp [Prod.map] }

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

Goal state before:
pp: case smul
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a✝ : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
a : A
ha : a ∈ I
b : A
hb : b ∈ J
n : ℕ
⊢ hI.dpow n (a • b) = hJ.dpow n (a • b)

Tactic:
rw [smul_eq_mul, hJ.dpow_mul hb, mul_comm a b, hI.dpow_mul ha,
      ← hJ.factorial_mul_dpow_eq_pow hb, ← hI.factorial_mul_dpow_eq_pow ha]

Goal state after:
case smul
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a✝ : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
a : A
ha : a ∈ I
b : A
hb : b ∈ J
n : ℕ
⊢ ↑n ! * hJ.dpow n b * hI.dpow n a = ↑n ! * hI.dpow n a * hJ.dpow n b
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
ι : Type u_4
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
a : ι → R
x : ι → M
⊢ dp R q (∑ i ∈ s, a i • x i) =
    ∑ k ∈ s.sym q, (∏ i ∈ s, a i ^ Multiset.count i ↑k) • ∏ i ∈ s, dp R (Multiset.count i ↑k) (x i)

Tactic:
dp_sum,

Goal state after:
R : Type u_2
M : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
a : ι → R
x : ι → M
⊢ ∑ k ∈ s.sym q, ∏ i ∈ s, dp R (Multiset.count i ↑k) (a i • x i) =
    ∑ k ∈ s.sym q, (∏ i ∈ s, a i ^ Multiset.count i ↑k) • ∏ i ∈ s, dp R (Multiset.count i ↑k) (x i)