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

Goal state before:
pp: case refine_2
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
f₁ f₂ : X → ℝ≥0∞
a✝¹ : Measurable f₁
a✝ : Measurable f₂
hf₁ : ∫⁻ (x : X), B.indicator 1 x * f₁ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₁ x ∂π x₀
hf₂ : ∫⁻ (x : X), B.indicator 1 x * f₂ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₂ x ∂π x₀
⊢ ∫⁻ (a : X), B.indicator 1 a * f₁ a ∂π x₀ + ∫⁻ (a : X), B.indicator 1 a * f₂ a ∂π x₀ =
    B.indicator 1 x₀ * (∫⁻ (a : X), f₁ a ∂π x₀ + ∫⁻ (a : X), f₂ a ∂π x₀)

pp: case refine_2.hg
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
f₁ f₂ : X → ℝ≥0∞
a✝¹ : Measurable f₁
a✝ : Measurable f₂
hf₁ : ∫⁻ (x : X), B.indicator 1 x * f₁ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₁ x ∂π x₀
hf₂ : ∫⁻ (x : X), B.indicator 1 x * f₂ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₂ x ∂π x₀
⊢ Measurable f₂

pp: case refine_2.hg
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
f₁ f₂ : X → ℝ≥0∞
a✝¹ : Measurable f₁
a✝ : Measurable f₂
hf₁ : ∫⁻ (x : X), B.indicator 1 x * f₁ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₁ x ∂π x₀
hf₂ : ∫⁻ (x : X), B.indicator 1 x * f₂ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₂ x ∂π x₀
⊢ Measurable fun x ↦ B.indicator 1 x * f₂ x

Tactic:
hf₁,

Goal state after:
case refine_2
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
f₁ f₂ : X → ℝ≥0∞
a✝¹ : Measurable f₁
a✝ : Measurable f₂
hf₁ : ∫⁻ (x : X), B.indicator 1 x * f₁ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₁ x ∂π x₀
hf₂ : ∫⁻ (x : X), B.indicator 1 x * f₂ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₂ x ∂π x₀
⊢ B.indicator 1 x₀ * ∫⁻ (x : X), f₁ x ∂π x₀ + ∫⁻ (a : X), B.indicator 1 a * f₂ a ∂π x₀ =
    B.indicator 1 x₀ * (∫⁻ (a : X), f₁ a ∂π x₀ + ∫⁻ (a : X), f₂ a ∂π x₀)

case refine_2.hg
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
f₁ f₂ : X → ℝ≥0∞
a✝¹ : Measurable f₁
a✝ : Measurable f₂
hf₁ : ∫⁻ (x : X), B.indicator 1 x * f₁ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₁ x ∂π x₀
hf₂ : ∫⁻ (x : X), B.indicator 1 x * f₂ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₂ x ∂π x₀
⊢ Measurable f₂

case refine_2.hg
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
B : Set X
f : X → ℝ≥0∞
x₀ : X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hB : MeasurableSet B
f₁ f₂ : X → ℝ≥0∞
a✝¹ : Measurable f₁
a✝ : Measurable f₂
hf₁ : ∫⁻ (x : X), B.indicator 1 x * f₁ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₁ x ∂π x₀
hf₂ : ∫⁻ (x : X), B.indicator 1 x * f₂ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₂ x ∂π x₀
⊢ Measurable fun x ↦ B.indicator 1 x * f₂ x
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst✝ : SFinite μ
s : Set Ω
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ (μ.tilted fun x ↦ t * X x) s = ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf X μ t)) ∂μ

Tactic:
rcases eq_zero_or_neZero μ with rfl | hμ
  · simp
  · simp_rw [tilted_mul_apply_mgf s, exp_sub, exp_cgf ht]

Goal state after:
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
⊢ f 1 * (P.real A * ∫ (ω : Ω), ∏ s, (g s) (X s ω) ∂P) + f 0 * ∫ (a : Ω), ∏ x, (g x) (X x a) ∂P -
      f 0 * (P.real A * ∫ (ω : Ω), ∏ s, (g s) (X s ω) ∂P) =
    ((P.restrict A).real Set.univ • f 1 + (P.restrict Aᶜ).real Set.univ • f 0) * ∫ (x : Ω), ∏ x_1, (g x_1) (X x_1 x) ∂P

Tactic:
simp [measureReal_compl₀ mA]
    ring

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

Goal state before:

Tactic:
cgf X (κ ω') t
  _ = log (mgf X (κ ω') t) := rfl
  _ ≤ log (exp (c * t ^ 2 / 2)) := by
    by_cases h0 : κ ω' = 0
    · simpa [h0] using by positivity
    gcongr
    · exact mgf_pos' h0 (h_int t)
    · exact h t
  _ ≤ c * t ^ 2 / 2 := by rw [log_exp]

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 : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, (κ ω') {ω | 0 < X ω} = 0

Tactic:
by
  have hs : {ω | 0 < X ω} = ⋃ ε : {ε : ℚ // 0 < ε}, {ω | ε ≤ X ω} := by
    ext ω
    simp only [Set.mem_ofPred_eq, Set.mem_iUnion, Subtype.exists, exists_prop]
    constructor
    · intro hp
      obtain ⟨q, h1, h2⟩ := exists_rat_btwn hp
      exact ⟨q, (q.cast_pos.1 h1), h2.le⟩
    · intro ⟨q, h1, h2⟩
      exact lt_of_lt_of_le (q.cast_pos.2 h1) h2
  have hb (ε : ℚ) : ∀ᵐ ω' ∂ν, 0 < ε → (κ ω') {ω | ε ≤ X ω} = 0 := by
    filter_upwards [h.measure_ge_le_exp_add ε, h.isFiniteMeasure] with ω' hm _ hε
    simp only [neg_mul, NNReal.coe_zero, zero_mul, zero_div, add_zero] at hm
    suffices (κ ω').real {ω | ε ≤ X ω} = 0 by simpa [Measure.real, ENNReal.toReal_eq_zero_iff]
    have hl : Filter.Tendsto (fun t ↦ rexp (-(t * ε))) Filter.atTop (𝓝 0) := by
      apply tendsto_exp_neg_atTop_nhds_zero.comp
      exact Filter.Tendsto.atTop_mul_const (ε.cast_pos.2 hε) (fun _ a ↦ a)
    apply le_antisymm
    · exact ge_of_tendsto hl (Filter.eventually_atTop.2 ⟨0, hm⟩)
    · exact measureReal_nonneg
  /- `ν`-almost everywhere, `{ω | 0 < X ω}` is a countable union of `κ ω'`-null sets. -/
  filter_upwards [ae_all_iff.2 hb] with ω' hn
  simp only [hs, measure_iUnion_null_iff, Subtype.forall]
  exact fun _ ↦ hn _

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 Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * (X ω + Y ω))) (⇑κ ∘ₘ ν)

Tactic:
simp_rw [mul_add, exp_add]

Goal state after:
Ω : 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
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * X ω) * rexp (t * Y ω)) (⇑κ ∘ₘ ν)
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]

Goal state after:
Ω : 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 : Ω), rexp (t * X x) * rexp (t * Y x) ∂κ ω' ≤
    (∫ (x : Ω), rexp (t * X x) ^ ↑p ∂κ ω') ^ (1 / ↑p) * (∫ (x : Ω), rexp (t * Y x) ^ ↑q ∂κ ω') ^ (1 / ↑q)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case pos.inr
Ω : 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 η
⊢ Integrable (fun ω ↦ rexp (t * (X ω.1 + Y ω.2))) (⇑(κ ⊗ₖ η) ∘ₘ ν)

Tactic:
simp_rw [mul_add, exp_add]

Goal state after:
case pos.inr
Ω : 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 η
⊢ Integrable (fun ω ↦ rexp (t * X ω.1) * rexp (t * Y ω.2)) (⇑(κ ⊗ₖ η) ∘ₘ ν)
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
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
hX_int : Integrable (fun y ↦ rexp (↑q * X y)) (κ ω')
hY_mgf : ∀ᵐ (b : Ω) ∂κ ω', ∀ (t : ℝ), mgf Y (η (ω', b)) t ≤ rexp (↑cY * t ^ 2 / 2)
h_int_mul : Integrable (fun ω ↦ rexp (↑q * (X ω.1 + Y ω.2))) ((κ ⊗ₖ η) ω')
⊢ (fun x ↦ rexp (↑q * X x) * ∫ (y : Ω''), rexp (↑q * Y y) ∂η (ω', x)) ≤ᵐ[κ ω'] fun x ↦
    rexp (↑q * X x) * rexp (↑cY * ↑q ^ 2 / 2)

Tactic:
filter_upwards [all_ae_of hY_mgf q] with ω hY_mgf
      gcongr
      exact hY_mgf

Goal state after:
Module: Mathlib.RepresentationTheory.Equiv

Goal state before:
pp: G : Type v
inst✝⁶ : Monoid G
V : Type v'
inst✝⁵ : AddCommMonoid V
W : Type w'
inst✝⁴ : AddCommMonoid W
k : Type u
inst✝³ : CommSemiring k
inst✝² : Module k V
inst✝¹ : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
inst✝ : DecidableEq α
i : α
v : V
w : W
⊢ (σ.finsuppTensorLeft ρ α).symm (single i (v ⊗ₜ[k] w)) = single i v ⊗ₜ[k] w

Tactic:
simp [finsuppTensorLeft]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * (X ω + Y ω))) μ

Tactic:
simp_rw [mul_add, exp_add]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * X ω) * rexp (t * Y ω)) μ
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF (fun ω ↦ X ω - ∫ (x : Ω), X x ∂μ) cX μ
hY : HasSubgaussianMGF (fun ω ↦ Y ω - ∫ (x : Ω), Y x ∂μ) cY μ
hindep : X ⟂ᵢ[μ] Y
h_le : ∫ (x : Ω), Y x ∂μ ≤ ∫ (x : Ω), X x ∂μ
⊢ μ.real {ω | X ω ≤ Y ω} =
    μ.real {ω | ∫ (x : Ω), X x ∂μ - ∫ (x : Ω), Y x ∂μ ≤ Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)}

Tactic:
congr with ω
    grind

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✝¹ : A
x✝ : ρ.IntertwiningMap σ
⊢ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ (x✝¹ • x✝).toLinearMap) ⋯ =
    (RingHom.id A) x✝¹ • LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (f.toLinearMap ∘ₗ x✝.toLinearMap) ⋯

Tactic:
by ext; simp [toLinearMap_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
x✝¹ x✝ : σ.IntertwiningMap τ
⊢ { toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ ((x✝¹ + x✝).toLinearMap ∘ₗ g.toLinearMap) ⋯,
      map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x✝¹.toLinearMap ∘ₗ g.toLinearMap) ⋯,
        map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x✝.toLinearMap ∘ₗ g.toLinearMap) ⋯,
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by ext; simp [toLinearMap_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
x✝¹ : A
x✝ : σ.IntertwiningMap τ
⊢ { toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ ((x✝¹ • x✝).toLinearMap ∘ₗ g.toLinearMap) ⋯,
      map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id A) x✝¹ •
      { toFun := fun g ↦ LinearMap.intertwiningMap_of_isIntertwiningMap ρ τ (x✝.toLinearMap ∘ₗ g.toLinearMap) ⋯,
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by ext; simp [toLinearMap_apply]

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

Goal state before:
pp: case succ.succ
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : StandardBorelSpace Ω
Y : ℕ → Ω → ℝ
cY : ℕ → ℝ≥0
ℱ : Filtration ℕ mΩ
inst✝ : IsZeroOrProbabilityMeasure μ
h_adapted : StronglyAdapted ℱ Y
h0 : HasSubgaussianMGF (Y 0) (cY 0) μ
n : ℕ
a✝ :
  ((∀ i < n - 1, HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (cY (i + 1)) μ) →
      HasSubgaussianMGF (fun ω ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ) →
    (∀ i < n + 1 - 1, HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (cY (i + 1)) μ) →
      HasSubgaussianMGF (fun ω ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
hn :
  (∀ i < n + 1 - 1, HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (cY (i + 1)) μ) →
    HasSubgaussianMGF (fun ω ↦ ∑ i ∈ Finset.range (n + 1), Y i ω) (∑ i ∈ Finset.range (n + 1), cY i) μ
h_subG : ∀ i < n + 1 + 1 - 1, HasCondSubgaussianMGF (↑ℱ i) ⋯ (Y (i + 1)) (cY (i + 1)) μ
⊢ HasSubgaussianMGF (fun ω ↦ ∑ i ∈ Finset.range (n + 1 + 1), Y i ω) (∑ i ∈ Finset.range (n + 1 + 1), cY i) μ

Tactic:
specialize hn fun i hi ↦ h_subG i (by lia)
      simp_rw [Finset.sum_range_succ _ (n + 1)]
      refine HasSubgaussianMGF.add_of_hasCondSubgaussianMGF (ℱ.le n) ?_ (h_subG n (by lia))
      refine HasSubgaussianMGF.trim (ℱ.le n) ?_ hn
      refine Finset.measurable_fun_sum (Finset.range (n + 1)) fun m hm ↦
        ((h_adapted m).mono (ℱ.mono ?_)).measurable
      simp only [Finset.mem_range] at hm
      lia

Goal state after:
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst✝⁷ : Group G
inst✝⁶ : Field k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : FiniteDimensional k V
inst✝² : AddCommGroup W
inst✝¹ : Module k W
inst✝ : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
g : G
⊢ ρ.dual.character g * σ.character g = ρ.character g⁻¹ * σ.character g

Tactic:
char_dual

Goal state after:
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst✝⁷ : Group G
inst✝⁶ : Field k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : FiniteDimensional k V
inst✝² : AddCommGroup W
inst✝¹ : Module k W
inst✝ : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
g : G
⊢ ρ.character g⁻¹ * σ.character g = ρ.character g⁻¹ * σ.character g
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: k : Type u
inst✝¹ : Field k
G : Type v
inst✝ : Group G
V W : FDRep k G
g : G
⊢ (of (dual V.ρ)).character g * W.character g = V.character g⁻¹ * W.character g

Tactic:
char_dual

Goal state after:
k : Type u
inst✝¹ : Field k
G : Type v
inst✝ : Group G
V W : FDRep k G
g : G
⊢ V.character g⁻¹ * W.character g = V.character g⁻¹ * W.character g
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : Monoid H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
σ : Representation k G A
ρ : Representation k G B
h : H
x : H → B
hx : x ∈ coindV φ ρ
g : G
h₁ : H
⊢ (LinearMap.funLeft k B fun x ↦ x * h) x (φ g * h₁) = (ρ g) ((LinearMap.funLeft k B fun x ↦ x * h) x h₁)

Tactic:
by
    simpa [mul_assoc] using hx g (h₁ * h)

Goal state after:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G✝ : Type v
H✝ : Type v'
inst✝⁴ : CommRing k
inst✝³ : Group G✝
inst✝² : Group H✝
φ✝ : G✝ →* H✝
A✝ : Rep k G✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
s : G
x : ↑A
y : ↑B
⊢ (((Representation.ind φ A.ρ).tprod B.ρ) (φ s)) ((IndV.mk φ A.ρ 1) x ⊗ₜ[k] y) - (IndV.mk φ A.ρ 1) x ⊗ₜ[k] y =
    (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ))
          (MonoidAlgebra.single 1 1 ⊗ₜ[k] (A.ρ s) x) ⊗ₜ[k]
        (B.ρ (φ s)) y -
      (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ))
          (MonoidAlgebra.single 1 1 ⊗ₜ[k] x) ⊗ₜ[k]
        y

Tactic:
simp [← Coinvariants.mk_inv_tmul]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
X✝ Y✝ : SimplexCategoryᵒᵖ
f : X✝ ⟶ Y✝
⊢ (cechNerveTerminalFrom (Action.ofMulAction G G)).map f ≫
      (limit.isoLimitCone (Action.ofMulActionLimitCone G fun x ↦ G)).hom =
    (limit.isoLimitCone (Action.ofMulActionLimitCone G fun x ↦ G)).hom ≫ (classifyingSpaceUniversalCover G).map f

Tactic:
refine IsLimit.hom_ext (Action.ofMulActionLimitCone.{u, 0} G fun _ => G).2 fun j => ?_
    dsimp only [cechNerveTerminalFrom, Pi.lift]
    rw [Category.assoc, limit.isoLimitCone_hom_π, limit.lift_π, Category.assoc]
    exact (limit.isoLimitCone_hom_π _ _).symm

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
r : k
x : ↑A
g : G
⊢ r • (A.ρ g) x - r • x = r • ((A.ρ g) x - x)

Tactic:
smul_sub

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
r : k
x : ↑A
g : G
⊢ r • (A.ρ g) x - r • x = r • (A.ρ g) x - r • x
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
r : k
x : G → ↑A
g : G × G
⊢ r • (A.ρ g.1) (x g.2) - r • x (g.1 * g.2) + r • x g.1 = r • ((A.ρ g.1) (x g.2) - x (g.1 * g.2)) + r • x g.1

Tactic:
smul_sub

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
r : k
x : G → ↑A
g : G × G
⊢ r • (A.ρ g.1) (x g.2) - r • x (g.1 * g.2) + r • x g.1 = r • (A.ρ g.1) (x g.2) - r • x (g.1 * g.2) + r • x g.1
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(cocycles₂ A)
g : G
⊢ (A.ρ g) (f (g⁻¹, g)) - f (g, g⁻¹) = f (1, 1) - f (g, 1)

Tactic:
have := (mem_cocycles₂_iff f).1 f.2 g g⁻¹ g

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(cocycles₂ A)
g : G
this : f (g * g⁻¹, g) + f (g, g⁻¹) = (A.ρ g) (f (g⁻¹, g)) + f (g, g⁻¹ * g)
⊢ (A.ρ g) (f (g⁻¹, g)) - f (g, g⁻¹) = f (1, 1) - f (g, 1)
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
xi : σ →₀ ℕ
hxi : xi ∈ x.support
⊢ (∃ si ∈ s, si ≤ xi) ↔ ∃ si ∈ s, (coeff xi x = 0 ∨ si ≤ xi) ∧ 1 ∣ coeff xi x

Tactic:
one_dvd,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
xi : σ →₀ ℕ
hxi : xi ∈ x.support
⊢ (∃ si ∈ s, si ≤ xi) ↔ ∃ si ∈ s, (coeff xi x = 0 ∨ si ≤ xi) ∧ True
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:

Tactic:
_ = leftRegular t⁻¹ ((η.hom.hom.app rightFDRep).hom (single u 1)) 1 := by simp
    _ = (η.hom.hom.app rightFDRep).hom (leftRegular t⁻¹ (single u 1)) 1 :=
      congrFun congr(($nat.symm).hom (single u 1)) 1
    _ = evalAlgHom _ _ s (leftRegular t⁻¹ (single u 1)) :=
      congr($hs (leftRegular t⁻¹ (single u 1)))
    _ = _ := by by_cases u = t * s <;> simp_all

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
γ : Type u_3
R : Type u_4
S : Type u_5
f : σ → τ
g : τ → γ
inst✝² : TendstoCofinite f
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x✝¹ x✝ : MvPowerSeries σ R
n✝ : τ →₀ ℕ
⊢ (coeff n✝) (renameFun f (x✝¹ + x✝)) = (coeff n✝) (renameFun f x✝¹ + renameFun f x✝)

Tactic:
simp [coeff_renameFun, Finset.sum_add_distrib]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
⊢ span {a} ∉ kaplanskySet (closure {r | Prime r}).toSubsemigroup

Tactic:
have hzero : 0 ∉ closure {r : R | Prime r} := fun h ↦ by
    rcases exists_multiset_of_mem_closure h with ⟨l, hl, hprod⟩
    exact not_prime_zero (hl 0 (Multiset.prod_eq_zero_iff.1 hprod))

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
hzero : 0 ∉ closure {r | Prime r}
⊢ span {a} ∉ kaplanskySet (closure {r | Prime r}).toSubsemigroup
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
g : G
a : A
⊢ IsCycle₁ (single g a) ↔ g⁻¹ • g • a = g⁻¹ • a

Tactic:
simp [IsCycle₁, eq_comm]

Goal state after: