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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : ConditionallyCompleteLinearOrderBot ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst✝⁴ : Zero E
inst✝³ : DenselyOrdered ι
inst✝² : FirstCountableTopology ι
inst✝¹ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
hp : IsStable 𝓕 p
inst✝ : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
hpτ : ∀ (n : ℕ), p (stoppedProcess (fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)) (τ n))
⊢ Locally p 𝓕 X P

Tactic:
refine ⟨_, hτ.isLocalizingSequence_biInf, fun n ↦ ?_⟩

Goal state after:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : ConditionallyCompleteLinearOrderBot ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst✝⁴ : Zero E
inst✝³ : DenselyOrdered ι
inst✝² : FirstCountableTopology ι
inst✝¹ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
hp : IsStable 𝓕 p
inst✝ : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
hpτ : ∀ (n : ℕ), p (stoppedProcess (fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)) (τ n))
n : ℕ
⊢ p (stoppedProcess (fun i ↦ {ω | ⊥ < ⨅ j, ⨅ (_ : j ≥ n), τ j ω}.indicator (X i)) fun ω ↦ ⨅ j, ⨅ (_ : j ≥ n), τ j ω)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : 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 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cX
q : ℝ≥0 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cY
ω' : Ω'
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 : ℝ
⊢ ∫ (x : Ω), (fun ω ↦ rexp (t * (X ω + Y ω))) x ∂κ ω' ≤
    (∫ (x : Ω), (fun ω ↦ rexp (t * X ω) ^ ↑p) x ∂κ ω') ^ (1 / ↑p) *
      (∫ (x : Ω), (fun ω ↦ rexp (t * Y ω) ^ ↑q) x ∂κ ω') ^ (1 / ↑q)

Tactic:
simp_rw [mul_add, exp_add]
        apply integral_mul_le_Lp_mul_Lq_of_nonneg
        · exact ⟨by simp [field, p, q], by positivity, by positivity⟩
        · exact ae_of_all _ fun _ ↦ exp_nonneg _
        · exact ae_of_all _ fun _ ↦ exp_nonneg _
        · simpa using (hlX t)
        · simpa using (hlY t)

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X Y : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
x : X.V
y : Y.V
r s : k
⊢ (μ X Y) (MonoidAlgebra.single x r ⊗ₜ[k] MonoidAlgebra.single y s) = MonoidAlgebra.single (x, y) (r * s)

Tactic:
by
  ext; simp [← toLinearMap_apply]

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

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
hm : m ≤ mΩ
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
c : ℝ≥0
h : HasCondSubgaussianMGF m hm X c μ
t : ℝ
h_eq : μ[fun ω ↦ rexp (t * X ω) | m] =ᵐ[μ.trim hm] fun ω ↦ ∫ (ω : Ω), rexp (t * X ω) ∂(condExpKernel μ m) ω
ω' : Ω
h_mgf : ∀ (t : ℝ), mgf X ((condExpKernel μ m) ω') t ≤ rexp (↑c * t ^ 2 / 2)
⊢ μ[fun ω ↦ rexp (t * X ω) | m] ω' = ∫ (ω : Ω), rexp (t * X ω) ∂(condExpKernel μ m) ω' →
    μ[fun ω ↦ rexp (t * X ω) | m] ω' ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
h_eq

Goal state after:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
hm : m ≤ mΩ
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
c : ℝ≥0
h : HasCondSubgaussianMGF m hm X c μ
t : ℝ
h_eq✝ : μ[fun ω ↦ rexp (t * X ω) | m] =ᵐ[μ.trim hm] fun ω ↦ ∫ (ω : Ω), rexp (t * X ω) ∂(condExpKernel μ m) ω
ω' : Ω
h_mgf : ∀ (t : ℝ), mgf X ((condExpKernel μ m) ω') t ≤ rexp (↑c * t ^ 2 / 2)
h_eq : μ[fun ω ↦ rexp (t * X ω) | m] ω' = ∫ (ω : Ω), rexp (t * X ω) ∂(condExpKernel μ m) ω'
⊢ μ[fun ω ↦ rexp (t * X ω) | m] ω' ≤ rexp (↑c * t ^ 2 / 2)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
hm : m ≤ mΩ
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
c : ℝ≥0
h : HasCondSubgaussianMGF m hm X c μ
t : ℝ
h_eq✝ : μ[fun ω ↦ rexp (t * X ω) | m] =ᵐ[μ.trim hm] fun ω ↦ ∫ (ω : Ω), rexp (t * X ω) ∂(condExpKernel μ m) ω
ω' : Ω
h_mgf : ∀ (t : ℝ), mgf X ((condExpKernel μ m) ω') t ≤ rexp (↑c * t ^ 2 / 2)
h_eq : μ[fun ω ↦ rexp (t * X ω) | m] ω' = ∫ (ω : Ω), rexp (t * X ω) ∂(condExpKernel μ m) ω'
⊢ μ[fun ω ↦ rexp (t * X ω) | m] ω' ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
h_eq

Goal state after:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
hm : m ≤ mΩ
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
c : ℝ≥0
h : HasCondSubgaussianMGF m hm X c μ
t : ℝ
h_eq✝ : μ[fun ω ↦ rexp (t * X ω) | m] =ᵐ[μ.trim hm] fun ω ↦ ∫ (ω : Ω), rexp (t * X ω) ∂(condExpKernel μ m) ω
ω' : Ω
h_mgf : ∀ (t : ℝ), mgf X ((condExpKernel μ m) ω') t ≤ rexp (↑c * t ^ 2 / 2)
h_eq : μ[fun ω ↦ rexp (t * X ω) | m] ω' = ∫ (ω : Ω), rexp (t * X ω) ∂(condExpKernel μ m) ω'
⊢ ∫ (ω : Ω), rexp (t * X ω) ∂(condExpKernel μ m) ω' ≤ rexp (↑c * t ^ 2 / 2)
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
K : ℕ
⊢ ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ ∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∫ (a : Ω), (truncation (X 0) ↑j ^ 2) a

Tactic:
by
        gcongr with j
        rw [(hident j).truncation.variance_eq]
        exact variance_le_expectation_sq (hX 0).truncation

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
U : Type u_5
inst✝⁷ : Semiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f✝ : V →ₗ[A] W
n : ℕ
f : ρ.IntertwiningMap σ
⊢ ∀ (g : G), (n • f.toLinearMap) ∘ₗ ρ g = σ g ∘ₗ (n • f.toLinearMap)

Tactic:
by simp [LinearMap.smul_comp, LinearMap.comp_smul, f.2]

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
U : Type u_5
inst✝¹³ : Semiring A
inst✝¹² : Monoid G
inst✝¹¹ : AddCommMonoid V✝
inst✝¹⁰ : AddCommMonoid W✝
inst✝⁹ : AddCommMonoid U
inst✝⁸ : Module A V✝
inst✝⁷ : Module A W✝
inst✝⁶ : Module A U
ρ✝ : Representation A G V✝
σ✝ : Representation A G W✝
τ✝ : Representation A G U
f✝¹ : V✝ →ₗ[A] W✝
V : Type u_6
W : Type u_7
P : Type u_8
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup P
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A P
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G P
f✝ : V →ₗ[A] W
z : ℤ
f : ρ.IntertwiningMap σ
⊢ ∀ (g : G), (z • f.toLinearMap) ∘ₗ ρ g = σ g ∘ₗ (z • f.toLinearMap)

Tactic:
by simp [LinearMap.smul_comp, LinearMap.comp_smul, f.2]

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
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f✝ : V →ₗ[A] W
a : A
f : ρ.IntertwiningMap σ
⊢ ∀ (g : G), (a • f.toLinearMap) ∘ₗ ρ g = σ g ∘ₗ (a • f.toLinearMap)

Tactic:
by simp [LinearMap.smul_comp, LinearMap.comp_smul, f.2]

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

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝¹ : StandardBorelSpace Ω
inst✝ : IsFiniteMeasure μ
Y : Ω → ℝ
cX cY : ℝ≥0
hm : m ≤ mΩ
hX : HasSubgaussianMGF X cX (μ.trim hm)
hY : HasCondSubgaussianMGF m hm Y cY μ
this : HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (cX + cY) (Measure.map Function.diag μ)
h_eq : X + Y = (fun p ↦ X p.1 + Y p.2) ∘ Function.diag
⊢ HasSubgaussianMGF (X + Y) (cX + cY) μ

Tactic:
h_eq

Goal state after:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝¹ : StandardBorelSpace Ω
inst✝ : IsFiniteMeasure μ
Y : Ω → ℝ
cX cY : ℝ≥0
hm : m ≤ mΩ
hX : HasSubgaussianMGF X cX (μ.trim hm)
hY : HasCondSubgaussianMGF m hm Y cY μ
this : HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (cX + cY) (Measure.map Function.diag μ)
h_eq : X + Y = (fun p ↦ X p.1 + Y p.2) ∘ Function.diag
⊢ HasSubgaussianMGF ((fun p ↦ X p.1 + Y p.2) ∘ Function.diag) (cX + cY) μ
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
A : Tendsto (fun i ↦ ∫ (a : Ω), truncation (X i) (↑i) a) atTop (𝓝 (∫ (a : Ω), X 0 a))
⊢ (fun n ↦ (∫ (a : Ω), (∑ i ∈ range n, truncation (X i) ↑i) a) - ↑n * ∫ (a : Ω), X 0 a) =o[atTop] Nat.cast

Tactic:
convert! Asymptotics.isLittleO_sum_range_of_tendsto_zero (tendsto_sub_nhds_zero_iff.2 A) using 1

Goal state after:
case e'_7
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
A : Tendsto (fun i ↦ ∫ (a : Ω), truncation (X i) (↑i) a) atTop (𝓝 (∫ (a : Ω), X 0 a))
⊢ (fun n ↦ (∫ (a : Ω), (∑ i ∈ range n, truncation (X i) ↑i) a) - ↑n * ∫ (a : Ω), X 0 a) = fun n ↦
    ∑ i ∈ range n, ((∫ (a : Ω), truncation (X i) (↑i) a) - ∫ (a : Ω), X 0 a)
Module: Mathlib.RepresentationTheory.Irreducible

Goal state before:
pp: G : Type u_1
k : Type u_2
inst✝³ : Monoid G
inst✝² : Field k
M : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : Module k[G] M
⊢ IsSimpleOrder (Submodule k[G] M) ↔ (ofModule M).IsIrreducible

Tactic:
exact OrderIso.isSimpleOrder_iff Subrepresentation.submoduleSubrepresentationOrderIso

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
⊢ ∀ {s : Set E} (hs : MeasurableSet s),
    ∀ᵐ (ω : Ω) ∂μ,
      Tendsto
        (fun n ↦
          (↑n)⁻¹ •
            ∑ i ∈ Finset.range n, (SimpleFunc.piecewise s hs (SimpleFunc.const E c) (SimpleFunc.const E 0)) (X i ω))
        atTop (𝓝 (∫ (x : Ω), (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const E c) (SimpleFunc.const E 0)) ∘ X 0) x ∂μ))

Tactic:
s

Goal state after:
case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
⊢ ∀ (hs : MeasurableSet s),
    ∀ᵐ (ω : Ω) ∂μ,
      Tendsto
        (fun n ↦
          (↑n)⁻¹ •
            ∑ i ∈ Finset.range n, (SimpleFunc.piecewise s hs (SimpleFunc.const E c) (SimpleFunc.const E 0)) (X i ω))
        atTop (𝓝 (∫ (x : Ω), (⇑(SimpleFunc.piecewise s hs (SimpleFunc.const E c) (SimpleFunc.const E 0)) ∘ X 0) x ∂μ))
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k✝ : Type u_1
inst✝¹³ : Field k✝
G✝ : Type u_2
inst✝¹² : Finite G✝
inst✝¹¹ : NeZero ↑(Nat.card G✝)
inst✝¹⁰ : Group G✝
V✝ : Type u_3
inst✝⁹ : AddCommGroup V✝
inst✝⁸ : Module k✝[G✝] V✝
W : Type u_4
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k✝[G✝] W
G : Type u_5
k : Type u_6
V : Type u_7
inst✝⁵ : Group G
inst✝⁴ : Field k
inst✝³ : Finite G
inst✝² : NeZero ↑(Nat.card G)
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
⊢ ρ.IsSemisimpleRepresentation

Tactic:
isSemisimpleRepresentation_iff_isSemisimpleModule_asModule

Goal state after:
k✝ : Type u_1
inst✝¹³ : Field k✝
G✝ : Type u_2
inst✝¹² : Finite G✝
inst✝¹¹ : NeZero ↑(Nat.card G✝)
inst✝¹⁰ : Group G✝
V✝ : Type u_3
inst✝⁹ : AddCommGroup V✝
inst✝⁸ : Module k✝[G✝] V✝
W : Type u_4
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k✝[G✝] W
G : Type u_5
k : Type u_6
V : Type u_7
inst✝⁵ : Group G
inst✝⁴ : Field k
inst✝³ : Finite G
inst✝² : NeZero ↑(Nat.card G)
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
⊢ IsSemisimpleModule k[G] ρ.asModule
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: 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
a : ↑A
⊢ (if h : (QuotientGroup.rightRel S) g g then A.ρ ⟨g * g⁻¹, ⋯⟩ else 0) a = a

Tactic:
dif_pos

Goal state after:
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
a : ↑A
⊢ (A.ρ ⟨g * g⁻¹, ⋯⟩) a = a

case hc
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
a : ↑A
⊢ (QuotientGroup.rightRel S) g g
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: case refine_2
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
⊢ (ρ g - LinearMap.id).range ≤ Coinvariants.ker ρ

Tactic:
rintro x ⟨y, rfl⟩
    simpa using Coinvariants.sub_mem_ker g y

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

Goal state before:
pp: case refine_2
k : Type u_1
G : Type u_2
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
this : Fintype G
x : MonoidAlgebra k G
hx : x ∈ ((linearCombination k fun x ↦ 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)).ker
⊢ x ∈ Coinvariants.ker (leftRegular k G)

Tactic:
· have : x = x.coeff.sum (fun g r => .single g r - .single 1 r) := by
      ext g
      by_cases hg : g = 1
      · simp_all [linearCombination, sum_apply', MonoidAlgebra.coeff_finsuppSum]
      · simp_all [sum_apply', MonoidAlgebra.coeff_finsuppSum]
    rw [this]
    exact Submodule.finsuppSum_mem _ _ _ _ fun g _ =>
      Coinvariants.mem_ker_of_eq g (.single 1 (x.coeff g)) _ (by simp)

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
i : ℕ
z : (Fin i → G) → ↑X.X₃
y : (Fin i → G) → ↑X.X₂
hy : (ConcreteCategory.hom ((cochainsMap (MonoidHom.id G) X.g).f i)) y = z
hz : (ConcreteCategory.hom ((inhomogeneousCochains X.X₃).d i (i + 1))) z = 0
x : (Fin (i + 1) → G) → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d i (i + 1))) y
⊢ (ConcreteCategory.hom (inhomogeneousCochains.d X.X₃ i)) z = 0

Tactic:
simpa [CochainComplex.of.d] using! hz

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
x y : G → ↑A
g : G × G
⊢ (A.ρ g.1) (x g.2 + y g.2) - (x (g.1 * g.2) + y (g.1 * g.2)) + (x g.1 + y g.1) =
    (A.ρ g.1) (x g.2) - x (g.1 * g.2) + x g.1 + ((A.ρ g.1) (y g.2) - y (g.1 * g.2) + y g.1)

Tactic:
rw [map_add, add_add_add_comm, add_sub_add_comm]

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 : ℕ
⊢ map (↑e.symm) (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ }) n ≫
      map (↑e) (ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ }) n =
    𝟙 (groupCohomology B n)

Tactic:
← groupCohomology.map_comp,

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 : ℕ
⊢ map ((↑e.symm).comp ↑e)
      ((resFunctor ↑e).map (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ }) ≫
        ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ })
      n =
    𝟙 (groupCohomology B 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
n✝ : ℕ
e : G ≃* H
e' : ↑B ≃ₗ[k] ↑A
he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map (↑e) (ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ }) n ≫
      map (↑e.symm) (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ }) n =
    𝟙 (groupCohomology A n)

Tactic:
← groupCohomology.map_comp,

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 : ℕ
⊢ map ((↑e).comp ↑e.symm)
      ((resFunctor ↑e.symm).map (ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ }) ≫
        ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ })
      n =
    𝟙 (groupCohomology A n)
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
⊢ (ConcreteCategory.hom ((inhomogeneousChains X.X₃).d 2 1)) ((ConcreteCategory.hom (chainsIso₂ X.X₃).inv) ↑z) = 0

Tactic:
by
    rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₂₁_comp_inv]; simp

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

Goal state before:
pp: case h.refine_2
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
g✝ : G ⧸ S
g h : G
hgh : (QuotientGroup.leftRel S) g h
⊢ ⟨↑x g - (A.ρ g) y + y, ⋯⟩ = ⟨↑x h - (A.ρ h) y + y, ⋯⟩

Tactic:
have := congr(A.ρ g $(h2 (g⁻¹ * h) <| QuotientGroup.leftRel_apply.1 hgh))

Goal state after:
case h.refine_2
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
g✝ : G ⧸ S
g h : G
hgh : (QuotientGroup.leftRel S) g h
this : (A.ρ g) (x (g⁻¹ * h)) = (A.ρ g) ((A.ρ (g⁻¹ * h)) y - y)
⊢ ⟨↑x g - (A.ρ g) y + y, ⋯⟩ = ⟨↑x h - (A.ρ h) y + y, ⋯⟩
Module: Mathlib.RingTheory.MvPolynomial.Ideal

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

Tactic:
obtain ⟨i, hi⟩ : x.support.Nonempty := by aesop

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : σ →₀ ℕ
hx : x ∈ ⇑degree ⁻¹' Set.Ici 1
i : σ
hi : i ∈ x.support
⊢ x ∈ (fun x ↦ (monomial x) 1) ⁻¹' ↑(Submodule.restrictScalars R (idealOfVars σ R))
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
x : τ →₀ ℕ
⊢ (coeff x) (renameFun f (p * q)) = (coeff x) (renameFun f p * renameFun f q)

Tactic:
simp only [coeff_renameFun, coeff_mul, sum_mul_sum, ← sum_product']

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 : τ →₀ ℕ
⊢ ∑ x ∈ ⋯.toFinset, ∑ p_1 ∈ antidiagonal x, (coeff p_1.1) p * (coeff p_1.2) q =
    ∑ p_1 ∈ antidiagonal x, ∑ x ∈ ⋯.toFinset ×ˢ ⋯.toFinset, (coeff x.1) p * (coeff x.2) q
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: case h₁
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : G × ↑A
⊢ (fun gv ↦ (A.ρ gv.1) gv.2 - gv.2) x ∈ ↑(ModuleCat.Hom.hom (d₁₀ A)).range

Tactic:
use single x.1⁻¹ x.2

Goal state after:
case h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : G × ↑A
⊢ (ModuleCat.Hom.hom (d₁₀ A)) (single x.1⁻¹ x.2) = (fun gv ↦ (A.ρ gv.1) gv.2 - gv.2) x
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
⊢ ∃ P ∈ kaplanskySet S, ∀ J ∈ C, J ≤ P

Tactic:
refine ⟨sSup C, ?_, fun _ hz ↦ le_sSup hz⟩
    rw [mem_kaplanskySet_iff, eq_empty_iff_forall_notMem]
    intro x hx
    rcases (Submodule.mem_sSup_of_directed ⟨_, hI⟩ hC₂.directedOn).1 hx.1 with ⟨J, hJ₁, hJ₂⟩
    have hx₂ : (J : Set R) ∩ S ≠ ∅ := nonempty_iff_ne_empty.1 ⟨x, hJ₂, hx.2⟩
    exact hx₂ (mem_kaplanskySet_iff.mp (hC hJ₁))

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : (Ideal.map constantCoeff I).FG
⊢ spanFinrank I ≤ spanFinrank (Ideal.map constantCoeff I) + 1

Tactic:
eq_span_insert_X_of_X_mem_of_span_eq hI (I.map constantCoeff).span_generators

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : (Ideal.map constantCoeff I).FG
⊢ spanFinrank (Ideal.span (insert X (⇑C '' generators (Ideal.map constantCoeff I)))) ≤
    spanFinrank (Ideal.map constantCoeff I) + 1
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case pos
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

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 spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_X_mem hP

Goal state after:
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
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

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

Tactic:
by
      suffices ∀ i j : ℕ, ∃ k, I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j by
        simpa only [smul_eq_mul, mul_top, Algebra.algebraMap_self, map_id, le_inf_iff] using! this
      intro i j
      exact ⟨max i j, pow_le_pow_right (le_max_left i j), pow_le_pow_right (le_max_right i j)⟩

Goal state after: