mathlib-initiative/mathlib-tactics huggingface dataset:
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 < x → x ≤ 0 → x ^ n = 0

Tactic:
intro _

Goal state after:
α : 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
⊢ x ≤ 0 → x ^ n = 0
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case pos.inr.refine_1
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
hη : IsMarkovKernel η
⊢ MemLp (fun ω ↦ rexp (t * X ω.1)) 2 (⇑(κ ⊗ₖ η) ∘ₘ ν)

pp: case pos.inr.refine_2
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
hη : IsMarkovKernel η
⊢ MemLp (fun ω ↦ rexp (t * Y ω.2)) 2 (⇑(κ ⊗ₖ η) ∘ₘ ν)

Tactic:
· have h := hX.memLp_exp_mul t 2
    simp only [ENNReal.coe_ofNat] at h
    have : κ ∘ₘ ν = ((κ ⊗ₖ η) ∘ₘ ν).map Prod.fst := by
      rw [Measure.map_comp _ _ measurable_fst, ← fst_eq, fst_compProd]
    rwa [this, memLp_map_measure_iff h.1 measurable_fst.aemeasurable] at h

Goal state after:
case pos.inr.refine_2
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
hη : IsMarkovKernel η
⊢ MemLp (fun ω ↦ rexp (t * Y ω.2)) 2 (⇑(κ ⊗ₖ η) ∘ₘ ν)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
⊢ HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ η) ν

Tactic:
by_cases hκ : IsSFiniteKernel κ
  swap; · simp [hκ]
  refine .of_rat (integrable_exp_add_compProd hX hY) fun q ↦ ?_
  filter_upwards [hX.mgf_le, hX.ae_integrable_exp_mul q, Measure.ae_ae_of_ae_compProd hY.mgf_le,
    Measure.ae_integrable_of_integrable_comp <| integrable_exp_add_compProd hX hY q]
    with ω' hX_mgf hX_int hY_mgf h_int_mul
  calc mgf (fun p ↦ X p.1 + Y p.2) ((κ ⊗ₖ η) ω') q
  _ = ∫ x, exp (q * X x) * ∫ y, exp (q * Y y) ∂(η (ω', x)) ∂(κ ω') := by
    simp_rw [mgf, mul_add, exp_add] at h_int_mul ⊢
    simp_rw [integral_compProd h_int_mul, integral_const_mul]
  _ ≤ ∫ x, exp (q * X x) * exp (cY * q ^ 2 / 2) ∂(κ ω') := by
    refine integral_mono_of_nonneg ?_ (hX_int.mul_const _) ?_
    · exact ae_of_all _ fun ω ↦ mul_nonneg (by positivity)
        (integral_nonneg (fun _ ↦ by positivity))
    · filter_upwards [all_ae_of hY_mgf q] with ω hY_mgf
      gcongr
      exact hY_mgf
  _ ≤ exp (↑(c + cY) * q ^ 2 / 2) := by
    rw [integral_mul_const, NNReal.coe_add, add_mul, add_div, exp_add]
    gcongr
    exact hX_mgf q

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())
Y : Ω → ℝ
h' : X =ᵐ[μ] Y
⊢ Kernel.HasSubgaussianMGF Y c (Kernel.const Unit μ) (Measure.dirac ())

Tactic:
apply h.congr

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())
Y : Ω → ℝ
h' : X =ᵐ[μ] Y
⊢ X =ᵐ[⇑(Kernel.const Unit μ) ∘ₘ Measure.dirac ()] Y
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
t : ℝ
p : ℝ≥0
⊢ MemLp (fun ω ↦ rexp (t * X ω)) (↑p) μ

Tactic:
rw [HasSubgaussianMGF_iff_kernel] at h

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())
t : ℝ
p : ℝ≥0
⊢ MemLp (fun ω ↦ rexp (t * X ω)) (↑p) μ
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
t : ℝ
⊢ cgf X μ t ≤ ↑c * t ^ 2 / 2

Tactic:
rw [HasSubgaussianMGF_iff_kernel] at h

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())
t : ℝ
⊢ cgf X μ t ≤ ↑c * t ^ 2 / 2
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
ε : ℝ
hε : 0 ≤ ε
⊢ μ.real {ω | ε ≤ X ω} ≤ rexp (-ε ^ 2 / (2 * ↑c))

Tactic:
rw [HasSubgaussianMGF_iff_kernel] at h

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())
ε : ℝ
hε : 0 ≤ ε
⊢ μ.real {ω | ε ≤ X ω} ≤ rexp (-ε ^ 2 / (2 * ↑c))
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e'_3.a
Ω : 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 : ℕ
a✝¹ : j ∈ range (u (N - 1))
hj : 0 < j
x✝ : ℕ
a✝ : x✝ ∈ {i ∈ range N | ↑j < ↑⌊c ^ i⌋₊}
⊢ (↑(u x✝) ^ 2)⁻¹ = 1 / ↑⌊c ^ x✝⌋₊ ^ 2

Tactic:
· simp only [u, one_div]

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

Goal state before:
pp: case hb
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
⊢ ∀ᵐ (ω : Ω) ∂μ, X ω - ∫ (x : Ω), X x ∂μ ∈ Set.Icc (a - ∫ (x : Ω), X x ∂μ) (b - ∫ (x : Ω), X x ∂μ)

pp: case hc
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
⊢ ∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ = 0

Tactic:
· filter_upwards [hb] with ω hab using by simpa using hab

Goal state after:
case hc
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
⊢ ∫ (x : Ω), X x - ∫ (x : Ω), X x ∂μ ∂μ = 0
Module: Mathlib.RepresentationTheory.Rep.Iso

Goal state before:
pp: case add
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : k[G]
x : V
⊢ ∀ (x_1 y : k[G]),
    f ((((lift k (V →ₗ[k] V) G) ρ) x_1) x) = (((lift k (W →ₗ[k] W) G) σ) x_1) (f x) →
      f ((((lift k (V →ₗ[k] V) G) ρ) y) x) = (((lift k (W →ₗ[k] W) G) σ) y) (f x) →
        f ((((lift k (V →ₗ[k] V) G) ρ) (x_1 + y)) x) = (((lift k (W →ₗ[k] W) G) σ) (x_1 + y)) (f x)

Tactic:
intro g h gw hw

Goal state after:
case add
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : k[G]
x : V
g h : k[G]
gw : f ((((lift k (V →ₗ[k] V) G) ρ) g) x) = (((lift k (W →ₗ[k] W) G) σ) g) (f x)
hw : f ((((lift k (V →ₗ[k] V) G) ρ) h) x) = (((lift k (W →ₗ[k] W) G) σ) h) (f x)
⊢ f ((((lift k (V →ₗ[k] V) G) ρ) (g + h)) x) = (((lift k (W →ₗ[k] W) G) σ) (g + h)) (f x)
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
X : ModuleCat k
Y : Rep k G
f : (trivialFunctor k G).obj X ⟶ Y
⊢ ∀ (c : ↑((trivialFunctor k G).obj X)), (Hom.hom f).toLinearMap c ∈ Y.ρ.invariants

Tactic:
intro _

Goal state after:
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
X : ModuleCat k
Y : Rep k G
f : (trivialFunctor k G).obj X ⟶ Y
c✝ : ↑((trivialFunctor k G).obj X)
⊢ (Hom.hom f).toLinearMap c✝ ∈ Y.ρ.invariants
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: case a.f
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
| fun g ↦ W.character g * V.character g⁻¹

Tactic:
intro _

Goal state after:
case a.f
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
x✝ : G
| W.character x✝ * V.character x✝⁻¹
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‖ ∂μ))
⊢ (∀ a' < 0, ∀ᶠ (b : ℕ) in atTop, a' < ‖(↑b)⁻¹ • ∑ i ∈ Finset.range b, X i ω - ∫ (x : Ω), X 0 x ∂μ‖) ∧
    ∀ a' > 0, ∀ᶠ (b : ℕ) in atTop, ‖(↑b)⁻¹ • ∑ i ∈ Finset.range b, X i ω - ∫ (x : Ω), X 0 x ∂μ‖ < a'

Tactic:
refine ⟨fun c hc ↦ Eventually.of_forall (fun n ↦ hc.trans_le (norm_nonneg _)), ?_⟩

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝ : SeparableSpace ↑s
this : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k ↦ Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
Y : ℕ → ℕ → Ω → E := fun k i ↦ ⇑(φ k) ∘ X i
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop
        (𝓝 (∫ (x : Ω), (fun ω ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω : ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
⊢ ∀ a' > 0, ∀ᶠ (b : ℕ) in atTop, ‖(↑b)⁻¹ • ∑ i ∈ Finset.range b, X i ω - ∫ (x : Ω), X 0 x ∂μ‖ < a'
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 : ↥(Representation.coindV φ A.ρ)
g : G
x✝ : H
⊢ (((linearCombination k ↑f ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ (Representation.ofMulAction k H H) (φ g)) ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    ((A.ρ g ∘ₗ linearCombination k ↑f ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ MonoidAlgebra.lsingle x✝) 1

Tactic:
simp [f.2 g]

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
⊢ (π.conjugate g) (i v) = v

Tactic:
by
  rw [conjugate_apply, ← i.map_smul, h, ← mul_smul, single_mul_single, mul_one, inv_mul_cancel,
    ← one_def, one_smul]

Goal state after:
Module: Mathlib.RepresentationTheory.FinGroupCharZero

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

Tactic:
← Rep.equivalenceModuleMonoidAlgebra.map_projective_iff,

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

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

Tactic:
refine le_antisymm (Submodule.span_le.2 ?_) ?_
  · rintro a ⟨⟨γ, α⟩, rfl⟩
    rcases mem_powers_iff_mem_zpowers.2 (hg γ) with ⟨i, rfl⟩
    induction i with | zero => exact ⟨0, by simp⟩ | succ n _ =>
    use (Fin.partialSum (fun (j : Fin (n + 1)) => ρ (g ^ (j : ℕ)) α) (Fin.last _))
    simpa using ρ.apply_sub_id_partialSum_eq _ _ _
  · rintro x ⟨y, rfl⟩
    simpa using Coinvariants.sub_mem_ker g y

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η : Aut (forget k G)
f g : G → k
nat :
  (forget k G).map mulRepHom ≫ η.hom.hom.app rightFDRep =
    (η.hom.hom.app rightFDRep ⊗ₘ η.hom.hom.app rightFDRep) ≫ (forget k G).map mulRepHom
tensor : ∀ (X Y : FDRep k G), η.hom.hom.app (X ⊗ Y) = η.hom.hom.app X ⊗ₘ η.hom.hom.app Y
⊢ let α := Hom.hom (η.hom.hom.app rightFDRep).hom;
  α (f * g) = α f * α g

Tactic:
exact ConcreteCategory.congr_hom ((CategoryTheory.forget _).congr_map nat) (f ⊗ₜ[k] g)

Goal state after:
Module: Mathlib.RingTheory.Noetherian.OfPrime

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : span (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
⊢ I.FG

Tactic:
have H k : ∃ r : R, ∃ p ∈ I, r * a + p = f k := by
      apply mem_span_singleton_sup.1
      rw [sup_comm, ← hf]
      exact mem_span_range_self

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : span (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
H : ∀ (k : Fin w✝¹), ∃ r, ∃ p ∈ I, r * a + p = f k
⊢ I.FG
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
⊢ Function.Injective ⇑(rename ⇑e)

Tactic:
intro _

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
a₁✝ : MvPowerSeries σ R
⊢ ∀ ⦃a₂ : MvPowerSeries σ R⦄, (rename ⇑e) a₁✝ = (rename ⇑e) a₂ → a₁✝ = 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
d : τ →₀ ℕ
x : σ
⊢ x ∉ ⋃ i ∈ ↑d.support, f ⁻¹' {i} → x ∉ {s | (coeff d) ((X ∘ f) s) ≠ 0}

Tactic:
intro _

Goal state after:
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
d : τ →₀ ℕ
x : σ
a✝ : x ∉ ⋃ i ∈ ↑d.support, f ⁻¹' {i}
⊢ x ∉ {s | (coeff d) ((X ∘ f) s) ≠ 0}
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
d : τ →₀ ℕ
x : σ
⊢ x ∈ {s | (coeff d) ((X ∘ f) s) ≠ 0} → x ∈ ⋃ i ∈ ↑d.support, f ⁻¹' {i}

Tactic:
by
      contrapose; intro _ _; classical simp_all [coeff_X]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this✝ : (𝓝 0).IsCountablyGenerated
this : (𝓤 R).IsCountablyGenerated
H : CompleteSpace R
f : ℕ → R
hf : ∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m
L : R
hL : Filter.map f Filter.atTop ≤ 𝓝 L
i : ℕ
⊢ ∃ N, ∀ (n : ℕ), N ≤ n → f n - L ∈ I ^ i

Tactic:
by
      simpa [sub_eq_neg_add] using (hI.hasBasis_nhds L).tendsto_right_iff.mp hL i

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

Goal state before:
pp: σ : Type u_2
τ : Type u_3
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
a : σ → MvPowerSeries τ R
ha : MvPowerSeries.HasSubst a
⊢ MvPowerSeries.subst a (subst (MvPowerSeries.X i) f) = subst (a i) f

Tactic:
subst,

Goal state after:
σ : Type u_2
τ : Type u_3
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
a : σ → MvPowerSeries τ R
ha : MvPowerSeries.HasSubst a
⊢ MvPowerSeries.subst a (MvPowerSeries.subst (fun x ↦ MvPowerSeries.X i) f) = subst (a i) f
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
a✝¹ : G × G
x✝ : ↑A
a✝ : K × K
⊢ ((ModuleCat.Hom.hom (mapShortComplexH1 (g.comp f) (φ ≫ resMap f ψ)).τ₁ ∘ₗ lsingle a✝¹) x✝) a✝ =
    ((ModuleCat.Hom.hom (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₁ ∘ₗ lsingle a✝¹) x✝) a✝

Tactic:
simp [Prod.map]

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

Goal state before:
pp: σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
d : σ →₀ ℕ
hd : d i = 0
hf : constantCoeff f = 0
⊢ ∀ (x : ℕ), d = single i x → (coeff x) f = 0

Tactic:
intro _

Goal state after:
σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
d : σ →₀ ℕ
hd : d i = 0
hf : constantCoeff f = 0
x✝ : ℕ
⊢ d = single i x✝ → (coeff x✝) f = 0
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
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
a✝¹ : G
x✝ : ↑A
a✝ : K
⊢ ((ModuleCat.Hom.hom (mapShortComplexH1 (g.comp f) (φ ≫ resMap f ψ)).τ₂ ∘ₗ lsingle a✝¹) x✝) a✝ =
    ((ModuleCat.Hom.hom (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₂ ∘ₗ lsingle a✝¹) x✝) a✝

Tactic:
simp [Prod.map]

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

Goal state before:
pp: case h
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (A.quotientToCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.quotientToCoinvariants S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.quotientToCoinvariants S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x)
z : ↥(cycles₁ (res S.subtype (A.toCoinvariants S)))
hz :
  (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype (A.toCoinvariants S))))) z) =
    (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
w : ↑(ModuleCat.of k (G × G →₀ ↑(A.toCoinvariants S)))
hzw :
  (ModuleCat.Hom.hom (d₂₁ (A.toCoinvariants S))) w =
    ↑((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype (A.toCoinvariants S))))) z) -
      ↑((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
Z : ↥S →₀ ↑A
hZ : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ Z = ↑z
W : G × G →₀ ↑A
hW : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ W = w
b : G →₀ ↑A := ↑x + (ConcreteCategory.hom (d₂₁ A)) W - (lmapDomain (↑A) k ⇑S.subtype) Z
hb : ∀ (g : G), b g ∈ Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)
β : G →₀ ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)) :=
  mapRange (Function.invFun ⇑(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype) ⋯ b
hβb : mapRange Subtype.val ⋯ β = b
α : ↥S →₀ ↑A
hα :
  (ModuleCat.Hom.hom (shortComplexH1 A).pOpcycles ∘ₗ
        ModuleCat.Hom.hom (mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂)
      α =
    (ModuleCat.Hom.hom (shortComplexH1 A).pOpcycles ∘ₗ
        ModuleCat.Hom.hom (mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f).τ₂)
      β
δ : G × G →₀ ↑A
hβ :
  (ModuleCat.Hom.hom (shortComplexH1 A).f) δ =
    (ModuleCat.Hom.hom (mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂) α -
      (ModuleCat.Hom.hom (mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f).τ₂) β
hαZ : (ConcreteCategory.hom (d₂₁ A)) (W + δ) = mapDomain Subtype.val (α + Z) - ↑x
⊢ (ModuleCat.Hom.hom (d₂₁ A)) (W + δ) =
    ↑((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype A)))) ⟨α + Z, ?w⟩) - ↑x

Tactic:
simp [hαZ, mapCycles₁_hom]

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

Goal state before:
pp: case mp
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
⊢ span {Submodule.IsPrincipal.generator p.contentIdeal} ≤ span {r} → C r ∣ p

Tactic:
intro _

Goal state after:
case mp
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
a✝ : span {Submodule.IsPrincipal.generator p.contentIdeal} ≤ span {r}
⊢ C r ∣ p
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ p.contentIdeal ≠ ⊤ → ∃ x, ∃ (_ : C x ∣ p), ¬IsUnit x

Tactic:
intro _

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
a✝ : p.contentIdeal ≠ ⊤
⊢ ∃ x, ∃ (_ : C x ∣ p), ¬IsUnit x
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ ↑p.coeffs ⊆ ↑(span {p.content})

Tactic:
intro _

Goal state after:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
a✝ : R
⊢ a✝ ∈ ↑p.coeffs → a✝ ∈ ↑(span {p.content})