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 g : X → ℝ≥0∞⦄,
    Disjoint (Function.support f) (Function.support g) →
      Measurable f →
        Measurable g →
          ∫⁻ (x : X), B.indicator 1 x * f x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f x ∂π x₀ →
            ∫⁻ (x : X), B.indicator 1 x * g x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), g x ∂π x₀ →
              ∫⁻ (x : X), B.indicator 1 x * (f + g) x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), (f + g) x ∂π x₀

Tactic:
rintro f₁ f₂ - _ _ hf₁ 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₀
⊢ ∫⁻ (x : X), B.indicator 1 x * (f₁ + f₂) x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), (f₁ + f₂) x ∂π x₀
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₀
⊢ ∫⁻ (x : X), B.indicator 1 x * f₁ x + B.indicator 1 x * f₂ x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f₁ x + f₂ x ∂π x₀

Tactic:
rw [lintegral_add_right, lintegral_add_right, hf₁, hf₂, mul_add]

Goal state after:
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.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
⊢ Measure.map (fun ω ↦ (k ω, g ω, f ω)) μ =
      ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ ↔
    Measure.map (fun x ↦ ((k x, g x), f x)) μ =
      ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun ω ↦ (k ω, g ω)) μ

Tactic:
let e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm

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
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
⊢ Measure.map (fun ω ↦ (k ω, g ω, f ω)) μ =
      ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ ↔
    Measure.map (fun x ↦ ((k x, g x), f x)) μ =
      ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun ω ↦ (k ω, g ω)) μ
Module: Mathlib.Probability.Moments.Tilted

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

Tactic:
simp_rw [tilted_mul_apply_eq_ofReal_integral_mgf s, exp_sub]

Goal state after:
case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst✝ : SFinite μ
s : Set Ω
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / mgf X μ t ∂μ) =
    ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a) / rexp (cgf X μ t) ∂μ)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case hx
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h✝ : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
h0 : ¬κ ω' = 0
⊢ 0 < mgf X (κ ω') t

pp: case hxy
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h✝ : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
h0 : ¬κ ω' = 0
⊢ mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
· exact mgf_pos' h0 (h_int t)

Goal state after:
case hxy
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h✝ : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
h0 : ¬κ ω' = 0
⊢ 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 Ω'
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
κ : Kernel Ω' Ω''
Y : Ω'' → Ω
X : Ω → ℝ
hY : Measurable Y
h : HasSubgaussianMGF X c (κ.map Y) ν
t : ℝ
h1 : Integrable (fun ω ↦ rexp (t * X ω)) (⇑(κ.map Y) ∘ₘ ν)
⊢ Integrable (fun ω ↦ rexp (t * (X ∘ Y) ω)) (⇑κ ∘ₘ ν)

Tactic:
rwa [← Measure.map_comp _ _ hY, integrable_map_measure h1.aestronglyMeasurable (by fun_prop)]
      at h1

Goal state after:
Module: Mathlib.RepresentationTheory.Subrepresentation

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

Tactic:
let _ : Module A[G] W := ρ.instModuleMonoidAlgebraAsModule

Goal state after:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
N : Submodule A[G] ρ.asModule
g : G
w : W
hw : w ∈ { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }
x✝ : Module A[G] W := ρ.instModuleMonoidAlgebraAsModule
⊢ (ρ g) w ∈ { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }
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
⊢ ∫ (x : α), truncation f A x ^ n ∂μ = ∫ (y : ℝ) in 0..A, y ^ n ∂Measure.map f μ

Tactic:
by
  have M : MeasurableSet (Set.Ioc 0 A) := measurableSet_Ioc
  have M' : MeasurableSet (Set.Ioc A 0) := measurableSet_Ioc
  rw [truncation_eq_of_nonneg h'f]
  change ∫ x, (fun z => indicator (Set.Ioc 0 A) id z ^ n) (f x) ∂μ = _
  rcases le_or_gt 0 A with (hA | hA)
  · rw [← integral_map (f := fun z => _ ^ n) hf.aemeasurable, intervalIntegral.integral_of_le hA,
      ← integral_indicator M]
    · simp only [indicator, zero_pow hn, id, ite_pow]
    · exact ((measurable_id.indicator M).pow_const n).aestronglyMeasurable
  · rw [← integral_map (f := fun z => _ ^ n) hf.aemeasurable, intervalIntegral.integral_of_ge hA.le,
      ← integral_indicator M']
    · simp only [Set.Ioc_eq_empty_of_le hA.le, zero_pow hn, Set.indicator_empty, integral_zero,
        zero_eq_neg]
      apply integral_eq_zero_of_ae
      have : ∀ᵐ x ∂Measure.map f μ, (0 : ℝ) ≤ x :=
        (ae_map_iff hf.aemeasurable measurableSet_Ici).2 (Eventually.of_forall h'f)
      filter_upwards [this] with x hx
      simp only [indicator, Set.mem_Ioc, Pi.zero_apply, ite_eq_right_iff, and_imp]
      intro _ h''x
      have : x = 0 := by linarith
      simp [this, zero_pow hn]
    · exact ((measurable_id.indicator M).pow_const n).aestronglyMeasurable

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case h.hab
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := ⋯
this : IsProbabilityMeasure ρ
i : ℕ
a✝ : i ∈ range N
⊢ ↑i ≤ ↑i + 1

pp: case h.hf
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := ⋯
this : IsProbabilityMeasure ρ
i : ℕ
a✝ : i ∈ range N
⊢ ∀ u ∈ Set.Icc (↑i) (↑i + 1), 0 ≤ 1

Tactic:
· simp only [le_add_iff_nonneg_right, zero_le_one]

Goal state after:
case h.hf
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := ⋯
this : IsProbabilityMeasure ρ
i : ℕ
a✝ : i ∈ range N
⊢ ∀ u ∈ Set.Icc (↑i) (↑i + 1), 0 ≤ 1
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
⊢ ∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∫ (a : Ω), (truncation X ↑j ^ 2) a ≤ 2 * ∫ (a : Ω), X a

Tactic:
have Y2 : ∀ n, 𝔼[Y n ^ 2] = ∫ x in 0..n, x ^ 2 ∂ρ := by
    intro n
    change 𝔼[fun x => Y n x ^ 2] = _
    rw [moment_truncation_eq_intervalIntegral_of_nonneg hint.1 two_ne_zero hnonneg]

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
⊢ ∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∫ (a : Ω), (truncation X ↑j ^ 2) a ≤ 2 * ∫ (a : Ω), X a
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
⊢ HasSubgaussianMGF (fun ω ↦ X ω - Y ω) (cX + cY) μ

Tactic:
simp_rw [sub_eq_add_neg]

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
⊢ HasSubgaussianMGF (fun ω ↦ X ω + -Y ω) (cX + cY) μ
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
f : G → k[G] := fun x ↦ single x 1
⊢ ⅟↑(Fintype.card G) • ∑ x, f (g * x) = ⅟↑(Fintype.card G) • ∑ x, f x

Tactic:
Function.Bijective.sum_comp (Group.mulLeft_bijective g) _

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
f : G → k[G] := fun x ↦ single x 1
⊢ ⅟↑(Fintype.card G) • ∑ i, f i = ⅟↑(Fintype.card G) • ∑ x, f 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
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
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun n ↦ F ∘ X n
this : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
hω : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
I : s.indicator (Function.const E c) = fun x ↦ s.indicator 1 x • c
⊢ Tendsto (fun n ↦ (↑n)⁻¹ • ∑ x ∈ Finset.range n, s.indicator 1 (X x ω) • c) atTop
    (𝓝 ((∫ (x : Ω), s.indicator 1 (X 0 x) ∂μ) • c))

Tactic:
convert! Tendsto.smul_const hω c using 1

Goal state after:
case e'_3
Ω : 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
F : E → ℝ := s.indicator 1
F_meas : Measurable F
Y : ℕ → Ω → ℝ := fun n ↦ F ∘ X n
this : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
ω : Ω
hω : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y i ω) atTop (𝓝 (∫ (x : Ω), Y 0 x ∂μ))
I : s.indicator (Function.const E c) = fun x ↦ s.indicator 1 x • c
⊢ (fun n ↦ (↑n)⁻¹ • ∑ x ∈ Finset.range n, s.indicator 1 (X x ω) • c) = fun x ↦
    ((↑x)⁻¹ • ∑ i ∈ Finset.range x, Y i ω) • c
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
x✝¹ x✝ : H
⊢ {
      toFun := fun f ↦
        (resFunctor φ).map (↑(leftRegular k H).leftRegularHomEquiv.symm (MonoidAlgebra.single (x✝¹ * x✝) 1)) ≫ f,
      map_add' := ⋯, map_smul' := ⋯ } =
    {
        toFun := fun f ↦
          (resFunctor φ).map (↑(leftRegular k H).leftRegularHomEquiv.symm (MonoidAlgebra.single x✝¹ 1)) ≫ f,
        map_add' := ⋯, map_smul' := ⋯ } *
      {
        toFun := fun f ↦
          (resFunctor φ).map (↑(leftRegular k H).leftRegularHomEquiv.symm (MonoidAlgebra.single x✝ 1)) ≫ f,
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by
    ext
    simp [homEquiv, mul_assoc]

Goal state after:
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 : res φ (leftRegular k H) ⟶ A
g : G
h : H
⊢ (fun h ↦ (Hom.hom f).toLinearMap (MonoidAlgebra.single h 1)) (φ g * h) =
    (A.ρ g) ((fun h ↦ (Hom.hom f).toLinearMap (MonoidAlgebra.single h 1)) h)

Tactic:
simp only [res_obj_V, res_obj_ρ, Representation.IntertwiningMap.toLinearMap_apply]

Goal state after:
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 : res φ (leftRegular k H) ⟶ A
g : G
h : H
⊢ (Hom.hom f) (MonoidAlgebra.single (φ g * h) 1) = (A.ρ g) ((Hom.hom f) (MonoidAlgebra.single h 1))
Module: Mathlib.RepresentationTheory.Continuous.TopRep

Goal state before:
pp: k : Type u
G : Type v
inst✝² : TopologicalSpace k
inst✝¹ : CommRing k
inst✝ : Monoid G
A B C : TopRep k G
f : A ⟶ B
r : k
g : B ⟶ C
⊢ f ≫ (r • g) = r • f ≫ g

Tactic:
ext; simp [hom_smul, ContIntertwiningMap.smul_comp]

Goal state after:
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
p : Submodule k[G] V
f : V →ₗ[k[G]] ↥p
hf : f ∘ₗ p.subtype = LinearMap.id
⊢ ∃ q, IsCompl p q

Tactic:
exact ⟨LinearMap.ker f, LinearMap.isCompl_of_proj <| DFunLike.congr_fun hf⟩

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommSemiring k
inst✝ : Monoid G
M N O : Rep k G
f : M ⟶ N
r : k
g : N ⟶ O
⊢ f ≫ (r • g) = r • f ≫ g

Tactic:
by
  ext
  simp [smul_hom, Representation.IntertwiningMap.smul_comp]

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
e✝ e : σ ↪ τ
⊢ killComplFun e 0 = 0

Tactic:
ext; simp [coeff_killComplFun]

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
e✝ e : σ ↪ τ
x✝¹ x✝ : MvPowerSeries τ R
⊢ killComplFun e (x✝¹ + x✝) = killComplFun e x✝¹ + killComplFun e x✝

Tactic:
ext; simp [coeff_killComplFun]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
⊢ SurjOn (⇑constantCoeff) (↑I) S

Tactic:
intro r hr

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
r : R
hr : r ∈ S
⊢ r ∈ ⇑constantCoeff '' ↑I
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case tg'
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H₁ : ∀ (n : ℕ), IsOpen[top] ↑(J ^ n)
H₂ : ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
⊢ IsTopologicalAddGroup R

Tactic:
apply (RingSubgroupsBasis.toRingFilterBasis _).toAddGroupFilterBasis.isTopologicalAddGroup

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

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
s : S
hs : ¬s = 0
⊢ s ∈ ↑(map f p).coeffs ∪ {0} ↔ s ∈ ⇑f '' ↑p.coeffs ∪ {0}

Tactic:
aesop (add simp mem_coeffs_iff)

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun x) =
    ↑v.intValuation.toMonoidWithZeroHom ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).1 *
      ↑((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom).domRestrict R⁰) ⋯)
            ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).2)⁻¹

Tactic:
Units.val_inv_eq_inv_val

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun x) =
    ↑v.intValuation.toMonoidWithZeroHom ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).1 *
      (↑((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom).domRestrict R⁰) ⋯)
            ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).2))⁻¹
Module: Mathlib.RingTheory.Regular.IsSMulRegular

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_4
M'' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M''
M''' : Type u_6
inst✝¹ : AddCommGroup M'''
inst✝ : Module R M'''
r : R
f₁ : M →ₗ[R] M'
f₂ : M' →ₗ[R] M''
f₃ : M'' →ₗ[R] M'''
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h : IsSMulRegular M''' r
this : IsSMulRegular (M'' ⧸ f₂.range) r
⊢ f₂.range ⊓ r • ⊤ ≤ r • Submodule.map f₂ ⊤

Tactic:
Submodule.map_top,

Goal state after:
R : Type u_1
M : Type u_3
M' : Type u_4
M'' : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
inst✝³ : AddCommGroup M''
inst✝² : Module R M''
M''' : Type u_6
inst✝¹ : AddCommGroup M'''
inst✝ : Module R M'''
r : R
f₁ : M →ₗ[R] M'
f₂ : M' →ₗ[R] M''
f₃ : M'' →ₗ[R] M'''
h₁₂ : Exact ⇑f₁ ⇑f₂
h₂₃ : Exact ⇑f₂ ⇑f₃
h : IsSMulRegular M''' r
this : IsSMulRegular (M'' ⧸ f₂.range) r
⊢ f₂.range ⊓ r • ⊤ ≤ r • f₂.range
Module: Mathlib.RingTheory.Regular.LinearMap

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
⊢ Subsingleton (N →ₗ[R] M) ↔ ∃ r ∈ annihilator R N, IsSMulRegular M r

Tactic:
refine ⟨fun hom0 ↦ ?_, fun ⟨r, mem_ann, reg⟩ ↦
    linearMap_subsingleton_of_mem_annihilator reg mem_ann⟩

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
⊢ ∃ r ∈ annihilator R N, IsSMulRegular M r
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
⊢ hI.dpow n (b * a) = hI.dpow n a * b ^ n

Tactic:
hI.dpow_mul ha,

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
⊢ b ^ n * hI.dpow n a = hI.dpow n a * b ^ n
Module: Mathlib.RingTheory.DividedPowers.Basic

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

Tactic:
hI.dpow_mul ha,

Goal state after:
case smul
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a✝ : A
hI : DividedPowers I
J : Ideal A
hJ : DividedPowers J
a : A
ha : a ∈ I
b : A
hb : b ∈ J
n : ℕ
⊢ b ^ n * hI.dpow n a = a ^ n * hJ.dpow n b
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: case succ
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
Nfin : Module.Finite R ↑N
Nsupp : Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      ∀ (rs : List R),
        (∀ r ∈ rs, r ∈ I) → RingTheory.Sequence.IsRegular (↑M) rs → rs.length = n → ∀ i < n, Subsingleton (Ext N M i)
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
rs : List R
mem : ∀ r ∈ rs, r ∈ I
reg : RingTheory.Sequence.IsRegular (↑M) rs
len : rs.length = n + 1
i : ℕ
hi : i < n + 1
le_rad : Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I
⊢ Subsingleton (Ext N M i)

Tactic:
rw [Module.support_eq_zeroLocus, PrimeSpectrum.zeroLocus_subset_zeroLocus_iff] at le_rad

Goal state after:
case succ
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
Nfin : Module.Finite R ↑N
Nsupp : Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      ∀ (rs : List R),
        (∀ r ∈ rs, r ∈ I) → RingTheory.Sequence.IsRegular (↑M) rs → rs.length = n → ∀ i < n, Subsingleton (Ext N M i)
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
rs : List R
mem : ∀ r ∈ rs, r ∈ I
reg : RingTheory.Sequence.IsRegular (↑M) rs
len : rs.length = n + 1
i : ℕ
hi : i < n + 1
le_rad : I ≤ (Module.annihilator R ↑N).radical
⊢ Subsingleton (Ext N M i)