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

Goal state before:
pp: case refine_2
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ s then Exists.choose ⋯ else Set.univ
h : μ[(⋂ i ∈ s, f i ⁻¹' g i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun ω ↦ 1 | m']
hg : ∀ i ∈ s, sets i = f i ⁻¹' g i
⊢ μ[(⋂ i ∈ s, sets i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(sets i).indicator fun ω ↦ 1 | m']

Tactic:
convert! h with i hi i hi <;> exact hg i hi

Goal state after:
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: case mp
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
a : ↑I
h_monotone : ∀ (s : X), Monotone fun x ↦ (κ s).real (Icc 0 x)
e : X × ↑I
y : ℝ
hyI : 0 ≤ y ∧ y ≤ 1
y_mem : (κ e.1).real (Icc 0 ⟨y, ⋯⟩) < ↑e.2
hy : ↑a < y
⊢ ∃ i, ↑a < ↑i ∧ ∃ (x : 0 ≤ i ∧ ↑i ≤ 1), (κ e.1).real (Icc 0 ⟨↑i, ⋯⟩) < ↑e.2

Tactic:
obtain ⟨q, hqa, hqy⟩ := exists_rat_btwn hy

Goal state after:
case mp
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
a : ↑I
h_monotone : ∀ (s : X), Monotone fun x ↦ (κ s).real (Icc 0 x)
e : X × ↑I
y : ℝ
hyI : 0 ≤ y ∧ y ≤ 1
y_mem : (κ e.1).real (Icc 0 ⟨y, ⋯⟩) < ↑e.2
hy : ↑a < y
q : ℚ
hqa : ↑a < ↑q
hqy : ↑q < y
⊢ ∃ i, ↑a < ↑i ∧ ∃ (x : 0 ≤ i ∧ ↑i ≤ 1), (κ e.1).real (Icc 0 ⟨↑i, ⋯⟩) < ↑e.2
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    f (A.indicator 1 ω) * ∏ s, (g s) (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
        A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω
h2 : ∀ (ω : Ω), f (A.indicator 1 ω) = A.indicator (fun x ↦ f 1) ω + Aᶜ.indicator (fun x ↦ f 0) ω
hg : ∀ {c : ℝ}, Integrable (fun ω ↦ c * ∏ s, (g s) (X s ω)) P
⊢ ∫ (x : Ω), (⇑f ∘ A.indicator 1) x * (∏ t, ⇑(g t) ∘ X t) x ∂P =
    (∫ (x : Ω), (⇑f ∘ A.indicator 1) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ X t) x ∂P

Tactic:
Finset.prod_apply,

Goal state after:
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    f (A.indicator 1 ω) * ∏ s, (g s) (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
        A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω
h2 : ∀ (ω : Ω), f (A.indicator 1 ω) = A.indicator (fun x ↦ f 1) ω + Aᶜ.indicator (fun x ↦ f 0) ω
hg : ∀ {c : ℝ}, Integrable (fun ω ↦ c * ∏ s, (g s) (X s ω)) P
⊢ ∫ (x : Ω), (⇑f ∘ A.indicator 1) x * ∏ c, (⇑(g c) ∘ X c) x ∂P =
    (∫ (x : Ω), (⇑f ∘ A.indicator 1) x ∂P) * ∫ (x : Ω), ∏ c, (⇑(g c) ∘ X c) x ∂P
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ}, MeasurableSet s → MeasurableSet (k ⁻¹' s)
h_left :
  ∀ {s : Set γ} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          (Measure.map (fun ω ↦ (k ω, f ω, g ω)) μ) (s ×ˢ t ×ˢ u) =
            (Measure.map (fun ω ↦ (ω, f ω, g ω)) μ) ((k ⁻¹' s) ×ˢ t ×ˢ u)
s : Set γ
t : Set β
u : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
a : Ω
haX : ((condDistrib f k μ) (k a)) t = (((condExpKernel μ (MeasurableSpace.comap k mγ)).map f) a) t
⊢ ((condDistrib g k μ) (k a)) u = (((condExpKernel μ (MeasurableSpace.comap k mγ)).map g) a) u →
    ((Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) (k a)) (s ×ˢ t ×ˢ u) =
      ((Kernel.id ×ₖ
            ((condExpKernel μ (MeasurableSpace.comap k mγ)).map f ×ₖ
              (condExpKernel μ (MeasurableSpace.comap k mγ)).map g))
          a)
        ((k ⁻¹' s) ×ˢ t ×ˢ u)

Tactic:
haT

Goal state after:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ}, MeasurableSet s → MeasurableSet (k ⁻¹' s)
h_left :
  ∀ {s : Set γ} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          (Measure.map (fun ω ↦ (k ω, f ω, g ω)) μ) (s ×ˢ t ×ˢ u) =
            (Measure.map (fun ω ↦ (ω, f ω, g ω)) μ) ((k ⁻¹' s) ×ˢ t ×ˢ u)
s : Set γ
t : Set β
u : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
a : Ω
haX : ((condDistrib f k μ) (k a)) t = (((condExpKernel μ (MeasurableSpace.comap k mγ)).map f) a) t
haT : ((condDistrib g k μ) (k a)) u = (((condExpKernel μ (MeasurableSpace.comap k mγ)).map g) a) u
⊢ ((Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) (k a)) (s ×ˢ t ×ˢ u) =
    ((Kernel.id ×ₖ
          ((condExpKernel μ (MeasurableSpace.comap k mγ)).map f ×ₖ
            (condExpKernel μ (MeasurableSpace.comap k mγ)).map g))
        a)
      ((k ⁻¹' s) ×ˢ t ×ˢ u)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
h_int : ∀ (n : ℤ), ∀ᵐ (ω' : Ω') ∂ν, Integrable (fun ω ↦ rexp (↑n * X ω)) (κ ω')
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')

Tactic:
← ae_all_iff

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
h_int : ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℤ), Integrable (fun ω ↦ rexp (↑i * X ω)) (κ a)
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ Integrable (fun x ↦ |X x| ^ ↑p * rexp (t * X x)) μ

Tactic:
exact integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet ht p.2

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑κ ∘ₘ ν)
h_mgf : ∀ (q : ℚ), ∀ᵐ (ω' : Ω') ∂ν, mgf X (κ ω') ↑q ≤ rexp (↑c * ↑q ^ 2 / 2)
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
← ae_all_iff

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑κ ∘ₘ ν)
h_mgf : ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℚ), mgf X (κ a) ↑i ≤ rexp (↑c * ↑i ^ 2 / 2)
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 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
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑κ ∘ₘ ν)
h_mgf : ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℚ), mgf X (κ a) ↑i ≤ rexp (↑c * ↑i ^ 2 / 2)
h_int' : ∀ (n : ℤ), ∀ᵐ (x : Ω') ∂ν, Integrable (fun ω ↦ rexp (↑n * X ω)) (κ x)
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')

Tactic:
← ae_all_iff

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑κ ∘ₘ ν)
h_mgf : ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℚ), mgf X (κ a) ↑i ≤ rexp (↑c * ↑i ^ 2 / 2)
h_int' : ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℤ), Integrable (fun ω ↦ rexp (↑i * X ω)) (κ a)
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
⊢ ∀ (a : Ω'), (κ a) {ω | 0 < (-X) ω} = 0 → (κ a) {ω | 0 < X ω} = 0 → X =ᵐ[κ a] 0

Tactic:
intro ω' h1 h2

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω' : Ω'
h1 : (κ ω') {ω | 0 < (-X) ω} = 0
h2 : (κ ω') {ω | 0 < X ω} = 0
⊢ X =ᵐ[κ ω'] 0
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p✝ q✝ : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp✝ : IsStable 𝓕 p✝
hq✝ : IsStable 𝓕 q✝
x✝ : Locally p✝ 𝓕 X P ∧ Locally q✝ 𝓕 X P
hpX✝ : Locally p✝ 𝓕 X P
hqX✝ : Locally q✝ 𝓕 X P
n : ℕ
p q : (ι → Ω → E) → Prop
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
i : ι
ω : Ω
⊢ stoppedProcess (fun i ↦ {ω | ⊥ < (hpX.localSeq ⊓ hqX.localSeq) n ω}.indicator (X i)) ((hpX.localSeq ⊓ hqX.localSeq) n)
      i ω =
    stoppedProcess
      (fun i ↦
        {ω | ⊥ < hqX.localSeq n ω}.indicator
          (stoppedProcess (fun i ↦ {ω | ⊥ < hpX.localSeq n ω}.indicator (X i)) (hpX.localSeq n) i))
      (hqX.localSeq n) i ω

Tactic:
simp_rw [stoppedProcess_indicator_comm, Pi.inf_apply, lt_inf_iff, inf_comm (hpX.localSeq n)]

Goal state after:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p✝ q✝ : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp✝ : IsStable 𝓕 p✝
hq✝ : IsStable 𝓕 q✝
x✝ : Locally p✝ 𝓕 X P ∧ Locally q✝ 𝓕 X P
hpX✝ : Locally p✝ 𝓕 X P
hqX✝ : Locally q✝ 𝓕 X P
n : ℕ
p q : (ι → Ω → E) → Prop
hp : IsStable 𝓕 p
hq : IsStable 𝓕 q
hpX : Locally p 𝓕 X P
hqX : Locally q 𝓕 X P
i : ι
ω : Ω
⊢ {ω | ⊥ < hpX.localSeq n ω ∧ ⊥ < hqX.localSeq n ω}.indicator (stoppedProcess X (hqX.localSeq n ⊓ hpX.localSeq n) i) ω =
    {ω | ⊥ < hqX.localSeq n ω}.indicator
      ({ω | ⊥ < hpX.localSeq n ω}.indicator (stoppedProcess (stoppedProcess X (hpX.localSeq n)) (hqX.localSeq n) i)) ω
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case inl
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
⊢ truncation f A x = ((Set.Ioc 0 A).indicator id ∘ f) x

Tactic:
simp only [truncation, indicator, hx, Set.mem_Ioc, id, Function.comp_apply]

Goal state after:
case inl
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
⊢ (if -A < f x ∧ f x ≤ A then f x else 0) = if True ∧ f x ≤ A then f x else 0
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
X : Action (Type w) G
g : G
x : X.V
⊢ ((linearize k G X) g) (MonoidAlgebra.single x 1) = MonoidAlgebra.single ((ConcreteCategory.hom (X.ρ g)) x) 1

Tactic:
by
  simp

Goal state after:
Module: Mathlib.RepresentationTheory.Equiv

Goal state before:
pp: G : Type v
inst✝³ : Monoid G
V : Type v'
inst✝² : AddCommMonoid V
k : Type u
inst✝¹ : CommSemiring k
inst✝ : Module k V
σ : Representation k G V
g : G
v : V
⊢ (σ.leftRegularMapEquiv.symm v) (MonoidAlgebra.single g 1) = (σ g) v

Tactic:
by
  simp

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

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

Tactic:
Finset.sum_insert his,

Goal state after:
case insert
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
c : ι → ℝ≥0
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
his : i ∉ s
h : (∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ) → HasSubgaussianMGF (fun ω ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
h_subG : ∀ i_1 ∈ insert i s, HasSubgaussianMGF (X i_1) (c i_1) μ
⊢ HasSubgaussianMGF (fun ω ↦ (X i + ∑ c ∈ s, X c) ω) (c i + ∑ i ∈ s, c i) μ
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✝⁵ : Semiring 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
ι : Type u_6
s : Finset ι
f : ι → ρ.IntertwiningMap σ
v : V
⊢ (∑ i ∈ s, f i) v = ∑ i ∈ s, (f i) v

Tactic:
by
  simp [← toLinearMap_apply _ _ (∑ _ ∈ s, _), toLinearMap_sum, LinearMap.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
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
f : σ.IntertwiningMap τ
x✝² x✝¹ : ρ.IntertwiningMap σ
x✝ : V
⊢ (LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ (x✝² + x✝¹).toLinearMap) ⋯).toLinearMap x✝ =
    (LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x✝².toLinearMap) ⋯ +
          LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x✝¹.toLinearMap) ⋯).toLinearMap
      x✝

Tactic:
simp [map_add, toLinearMap_apply]

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
α : Type u
inst✝ : DecidableEq α
i : α
x : ↑A
⊢ (A.finsuppToCoinvariantsTensorFree α) (single i x) =
    (Coinvariants.mk (A.ρ.tprod (Representation.free k G α))) (x ⊗ₜ[k] single i (MonoidAlgebra.single 1 1))

Tactic:
simp [finsuppToCoinvariantsTensorFree, Representation.finsuppTensorRight, Equiv.mk_symm]

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 (equivalenceModuleMonoidAlgebra.functor.obj V)

Tactic:
← IsProjective.iff_projective

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
⊢ Module.Projective (MonoidAlgebra k G) ↑(equivalenceModuleMonoidAlgebra.functor.1 V)
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : CommRing k
inst✝³ : Group G
inst✝² : Group H
φ : G →* H
A : Type u_4
inst✝¹ : AddCommGroup A
inst✝ : Module k A
ρ : Representation k G A
h₁ h₂ : H
a : A
⊢ ((ind φ ρ) h₁) ((IndV.mk φ ρ h₂) a) = (IndV.mk φ ρ (h₂ * h₁⁻¹)) a

Tactic:
by
  simp

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
A : Rep k G
n : ℕ
r : k
f : (Fin n → G) → ↑A
x✝ : Fin (n + 1) → G
⊢ (A.ρ (x✝ 0)) ((r • f) fun i ↦ x✝ i.succ) + ∑ j, (-1) ^ (↑j + 1) • (r • f) (j.contractNth (fun x1 x2 ↦ x1 * x2) x✝) =
    ((RingHom.id k) r • fun g ↦
        (A.ρ (g 0)) (f fun i ↦ g i.succ) + ∑ j, (-1) ^ (↑j + 1) • f (j.contractNth (fun x1 x2 ↦ x1 * x2) g))
      x✝

Tactic:
simp [Finset.smul_sum, ← smul_assoc, mul_comm r]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n : ℕ
⊢ (inhomogeneousCochains A).d n (n + 1) = d A n

Tactic:
by
  simp

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝ : ↑((standardComplex k G).X 1)
⊢ (forget₂ToModuleCat k G).d 1 0 ≫ (forget₂ (Rep k G) (ModuleCat k)).map (ε k G) = 0

Tactic:
← forget₂ToModuleCatHomotopyEquiv_f_0_eq,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝ : ↑((standardComplex k G).X 1)
⊢ (forget₂ToModuleCat k G).d 1 0 ≫ (forget₂ToModuleCatHomotopyEquiv k G).hom.f 0 = 0
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic

Goal state before:
pp: k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
⊢ ((A.coinvariantsTensorFreeLEquiv (Fin (n + 1 + 1) → G)).toModuleIso.inv ≫
        (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1 + 1) (n + 1) ≫
          (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G)).toModuleIso.hom) ≫
      inhomogeneousChains.d A n =
    0

Tactic:
inhomogeneousChains.d_eq

Goal state after:
k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
⊢ ((A.coinvariantsTensorFreeLEquiv (Fin (n + 1 + 1) → G)).toModuleIso.inv ≫
        (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1 + 1) (n + 1) ≫
          (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G)).toModuleIso.hom) ≫
      (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G)).toModuleIso.inv ≫
        (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n ≫
          (A.coinvariantsTensorFreeLEquiv (Fin n → G)).toModuleIso.hom =
    0
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ π A 0 ≫ (H0IsoOfIsTrivial A).hom = iCocycles A 0 ≫ (cochainsIso₀ A).hom

Tactic:
by
  simp

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
C : ↑(H2 A) → Prop
x : ↑(H2 A)
h : ∀ (x : ↥(cocycles₂ A)), C ((ConcreteCategory.hom (H2π A)) x)
y : ↑(cocycles A 2)
⊢ C ((ConcreteCategory.hom (π A 2)) y)

Tactic:
by simpa [H2π] using h ((isoCocycles₂ A).hom y)

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
⊢ cocyclesMap f φ 0 ≫ (cocyclesIso₀ B).hom ≫ (shortComplexH0 B).f =
    (cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f ≫ Hom.toModuleCatHom φ

Tactic:
by
  simp

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
⊢ mapCocycles₁ f φ ≫ (shortComplexH1 B).moduleCatLeftHomologyData.i =
    (shortComplexH1 A).moduleCatLeftHomologyData.i ≫ cochainsMap₁ f φ

Tactic:
by
  simp

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
X : FDRep k G
v : ↑X.V
⊢ ∑ s, single 1 1 s • (X.ρ s⁻¹) v = v

Tactic:
by
  simp

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
⊢ mapCocycles₂ f φ ≫ (shortComplexH2 B).moduleCatLeftHomologyData.i =
    (shortComplexH2 A).moduleCatLeftHomologyData.i ≫ cochainsMap₂ f φ

Tactic:
by
  simp

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

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

Tactic:
Submodule.span_le,

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ (fun x ↦ (monomial x) 1) '' ⇑degree ⁻¹' Set.Ici 1 ⊆ ↑(Submodule.restrictScalars R (idealOfVars σ R))
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: A : Type u_3
σ : Type u_4
inst✝ : CommRing A
I : Ideal (MvPolynomial σ A)
⊢ (↑↑(Ideal.Quotient.mk I)).toFun = eval₂ (algebraMap A (MvPolynomial σ A ⧸ I)) fun d ↦ (Ideal.Quotient.mk I) (X d)

Tactic:
by
  ext d
  simp_rw [RingHom.toFun_eq_coe, ← Ideal.Quotient.mkₐ_eq_mk A, mkₐ_eq_aeval, aeval_X, aeval,
    AlgHom.coe_mk, coe_eval₂Hom]

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

Goal state before:
pp: case refine_2
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})
r p : Fin w✝¹ → R
p_mem_I : ∀ (k : Fin w✝¹), p k ∈ I
Hf : ∀ (k : Fin w✝¹), r k * a + p k = f k
y : R
hy : y ∈ I
s : Fin w✝¹ → R
H : ∑ x, s x * p x + (∑ i, s i * r i) * a = y
⊢ ∃ y_1 ∈ span (Set.range p), ∃ z ∈ span (Set.range fun a_1 ↦ a • i a_1), y_1 + z = y

Tactic:
refine ⟨(∑ k, s k * p k), sum_mem _ (fun _ _ ↦ mul_mem_left _ _ mem_span_range_self),
        (∑ k, s k * r k) * a, ?_, H⟩

Goal state after:
case refine_2
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})
r p : Fin w✝¹ → R
p_mem_I : ∀ (k : Fin w✝¹), p k ∈ I
Hf : ∀ (k : Fin w✝¹), r k * a + p k = f k
y : R
hy : y ∈ I
s : Fin w✝¹ → R
H : ∑ x, s x * p x + (∑ i, s i * r i) * a = y
⊢ (∑ k, s k * r k) * a ∈ span (Set.range fun a_1 ↦ a • i a_1)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
g h : G
a : ↑A
⊢ single (h, 1) ((A.ρ g⁻¹) a) - single (g * h, 1) a ∈ boundaries₂ A

Tactic:
use single (g, h, 1) a
  simp [d₃₂]

Goal state after: