mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Decision.BayesEstimator

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst✝⁴ : StandardBorelSpace Θ
inst✝³ : Nonempty Θ
hl : Measurable (Function.uncurry ℓ)
P : Kernel Θ 𝓧
inst✝² : IsFiniteKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsSFiniteKernel κ
π : Measure Θ
inst✝ : IsFiniteMeasure π
⊢ ⇑(Kernel.id ∥ₖ κ) ∘ₘ π ⊗ₘ P = ⇑(Kernel.id ∥ₖ κ) ∘ₘ ⇑(P†π ×ₖ Kernel.id) ∘ₘ ⇑P ∘ₘ π

Tactic:
rw [posterior_prod_id_comp]

Goal state after:
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0

Tactic:
rw [setLIntegral_congr_fun measurableSet_Iio
      (fun x (hx : x < 0) ↦ gammaPDF_of_neg hx), lintegral_zero]

Goal state after:
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: p : ℝ
n : ℕ
hp_pos : 0 < p
hp_lt_one : p < 1
⊢ 0 < geometricPMFReal p n

Tactic:
by
  rw [geometricPMFReal]
  positivity [sub_pos.mpr hp_lt_one]

Goal state after:
Module: Mathlib.Probability.Kernel.Category.Stoch

Goal state before:
pp: X Y : Stoch
κ : X ⟶ Y
inst✝ : Deterministic κ
⊢ κ.hom.hom ∥ₖ κ.hom.hom ∘ₖ copy X.obj.carrier = copy Y.obj.carrier ∘ₖ κ.hom.hom

Tactic:
have := Deterministic.copy_natural κ.hom
    rw [SFinKer.Hom.ext_iff] at this
    dsimp at this
    rw [id_parallelComp_comp_parallelComp_id] at this
    exact this.symm

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

Goal state before:
pp: case inl
α : Type u_1
mα : MeasurableSpace α
κ η : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
hη : η.Invariant μ
h✝ : IsEmpty α
⊢ (κ ∘ₖ η).Invariant μ

pp: case inr
α : Type u_1
mα : MeasurableSpace α
κ η : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
hη : η.Invariant μ
hα : Nonempty α
⊢ (κ ∘ₖ η).Invariant μ

Tactic:
· exact Subsingleton.elim _ _

Goal state after:
case inr
α : Type u_1
mα : MeasurableSpace α
κ η : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
hη : η.Invariant μ
hα : Nonempty α
⊢ (κ ∘ₖ η).Invariant μ
Module: Mathlib.Probability.Kernel.Proper

Goal state before:
pp: X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
A : Set X
hA : MeasurableSet A
B : Set X
hB : MeasurableSet B
x : X
⊢ ((π x).restrict B) A = B.indicator 1 x * (π x) A ↔ (π x) (A ∩ B) = B.indicator 1 x * (π x) A

Tactic:
Measure.restrict_apply hA

Goal state after:
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
A : Set X
hA : MeasurableSet A
B : Set X
hB : MeasurableSet B
x : X
⊢ (π x) (A ∩ B) = B.indicator 1 x * (π x) A ↔ (π x) (A ∩ B) = B.indicator 1 x * (π x) A
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_sf_min : SigmaFinite (μ.trim ⋯)
this :
  ∀ᵐ (x : Ω) ∂μ,
    x ∈ {x | τ x ≤ σ x} → μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
⊢ ∀ᵐ (x : Ω) ∂μ,
    x ∈ {ω | σ ω ≤ τ ω}ᶜ → μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x

Tactic:
filter_upwards [this] with x hx hx_mem

Goal state after:
Ω : Type u_1
E : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : CompleteSpace E
ι : Type u_3
inst✝¹⁰ : LinearOrder ι
inst✝⁹ : LocallyFiniteOrder ι
inst✝⁸ : OrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : DiscreteTopology ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : BorelSpace ι
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
ℱ : Filtration ι m
τ σ : Ω → WithTop ι
f : ι → Ω → E
inst✝ : SigmaFiniteFiltration μ ℱ
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
n : ι
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
h_sf_min : SigmaFinite (μ.trim ⋯)
this :
  ∀ᵐ (x : Ω) ∂μ,
    x ∈ {x | τ x ≤ σ x} → μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
x : Ω
hx : τ x ≤ σ x → μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
hx_mem : x ∈ {ω | σ ω ≤ τ ω}ᶜ
⊢ μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case pos
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hY : HasSubgaussianMGF Y cY κ ν
hX0 : cX = 0
hX : HasSubgaussianMGF X 0 κ ν
⊢ Y =ᵐ[⇑κ ∘ₘ ν] fun ω ↦ X ω + Y ω

Tactic:
filter_upwards [ae_eq_zero_of_hasSubgaussianMGF_zero' hX] with ω hX0 using by simp [hX0]

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

Goal state before:
pp: case pos.mgf_le
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η (⇑κ ∘ₘ ν)
hν : SFinite ν
hκ : IsSFiniteKernel κ
⊢ ∀ᵐ (ω' : Ω' × Ω) ∂ν ⊗ₘ κ, ∀ (t : ℝ), mgf Y ((prodMkLeft Ω' η) ω') t ≤ rexp (↑cY * t ^ 2 / 2)

Tactic:
have h2 := h.mgf_le
    rw [← Measure.snd_compProd, Measure.snd] at h2
    exact ae_of_ae_map (by fun_prop) h2

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

Goal state before:
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 η
h : MemLp (fun ω ↦ rexp (t * Y ω)) (↑2) (⇑η ∘ₘ ν ⊗ₘ κ)
⊢ MemLp (fun ω ↦ rexp (t * Y ω.2)) 2 (⇑(κ ⊗ₖ η) ∘ₘ ν)

Tactic:
ENNReal.coe_ofNat,

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 η
h : MemLp (fun ω ↦ rexp (t * Y ω)) 2 (⇑η ∘ₘ ν ⊗ₘ κ)
⊢ MemLp (fun ω ↦ rexp (t * Y ω.2)) 2 (⇑(κ ⊗ₖ η) ∘ₘ ν)
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∑ i ∈ range N, ∫ (x : ℝ) in ↑i..↑(i + 1), x + 1 ∂ρ = ∫ (x : ℝ) in 0..↑N, x + 1 ∂ρ

Tactic:
by
        rw [intervalIntegral.sum_integral_adjacent_intervals fun k _ => ?_]
        · norm_cast
        · exact (continuous_id.add continuous_const).intervalIntegrable _ _

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: case e'_2
G : Type v
inst✝¹ : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
x : X.V
y : Y.V
z : Z.V
⊢ (MonoidAlgebra.tensorEquiv k)
      ((MonoidAlgebra.tensorEquiv k) ((MonoidAlgebra.lsingle x) 1 ⊗ₜ[k] (MonoidAlgebra.lsingle y) 1) ⊗ₜ[k]
        (MonoidAlgebra.lsingle z) 1) =
    MonoidAlgebra.single ((x, y), z) 1

pp: case e'_3
G : Type v
inst✝¹ : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
x : X.V
y : Y.V
z : Z.V
⊢ (MonoidAlgebra.tensorEquiv k)
      ((MonoidAlgebra.lsingle x) 1 ⊗ₜ[k]
        (MonoidAlgebra.tensorEquiv k) ((MonoidAlgebra.lsingle y) 1 ⊗ₜ[k] (MonoidAlgebra.lsingle z) 1)) =
    MonoidAlgebra.single ((ConcreteCategory.hom (α_ X Y Z).hom.hom) ((x, y), z)) 1

Tactic:
all_goals with_reducible simp

Goal state after:
Module: Mathlib.RepresentationTheory.Action

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

Tactic:
linearize_single

Goal state after:
k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
X : Type w
g : G
x : X
⊢ MonoidAlgebra.single ((ConcreteCategory.hom ((Action.trivial G X).ρ g)) x) 1 = MonoidAlgebra.single x 1
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: case mp
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
X Y : Rep k G
f : ↑X →ₗ[k] ↑Y
g : G
h : Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹ = f
⊢ f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f

Tactic:
← h

Goal state after:
case mp
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
X Y : Rep k G
f : ↑X →ₗ[k] ↑Y
g : G
h : Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹ = f
⊢ (Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹) ∘ₗ X.ρ g = Y.ρ g ∘ₗ f
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✝⁷ : Monoid 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
⊢ (ρ.tprod σ).character = ρ.character * σ.character

Tactic:
ext g

Goal state after:
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst✝⁷ : Monoid 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
⊢ (ρ.tprod σ).character g = (ρ.character * σ.character) g
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✝⁵ : Monoid G
inst✝⁴ : Field k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
σ : Representation k G W
φ : ρ.Equiv σ
⊢ ρ.character = σ.character

Tactic:
ext g

Goal state after:
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : Monoid G
inst✝⁴ : Field k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
σ : Representation k G W
φ : ρ.Equiv σ
g : G
⊢ ρ.character g = σ.character g
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: k : Type u
inst✝¹ : Field k
G : Type v
inst✝ : Monoid G
V W : FDRep k G
⊢ (V ⊗ W).character = V.character * W.character

Tactic:
ext g

Goal state after:
k : Type u
inst✝¹ : Field k
G : Type v
inst✝ : Monoid G
V W : FDRep k G
g : G
⊢ (V ⊗ W).character g = (V.character * W.character) g
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: k : Type u
inst✝¹ : Field k
G : Type v
inst✝ : Monoid G
V W : FDRep k G
i : V ≅ W
⊢ V.character = W.character

Tactic:
ext g

Goal state after:
k : Type u
inst✝¹ : Field k
G : Type v
inst✝ : Monoid G
V W : FDRep k G
i : V ≅ W
g : G
⊢ V.character g = W.character g
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 ∂μ))
x✝ : E
⊢ s.indicator (Function.const E c) x✝ = s.indicator 1 x✝ • c

Tactic:
← indicator_smul_const_apply

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
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 ∂μ))
x✝ : E
⊢ s.indicator (Function.const E c) x✝ = s.indicator (fun x ↦ 1 x • c) 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 ∂μ))
k : ℕ
G : ℕ → E → ℝ := fun k x ↦ ‖x - (φ k) x‖
G_meas : ∀ (k : ℕ), Measurable (G k)
⊢ ∀ᵐ (a : Ω) ∂μ,
    Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) a‖) / ↑n) atTop
      (𝓝 (∫ (x : Ω), (fun ω ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))

Tactic:
have I : ∀ k i, (fun ω ↦ ‖(X i - Y k i) ω‖) = (G k) ∘ (X i) := fun k i ↦ rfl

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 ∂μ))
k : ℕ
G : ℕ → E → ℝ := fun k x ↦ ‖x - (φ k) x‖
G_meas : ∀ (k : ℕ), Measurable (G k)
I : ∀ (k i : ℕ), (fun ω ↦ ‖(X i - Y k i) ω‖) = G k ∘ X i
⊢ ∀ᵐ (a : Ω) ∂μ,
    Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) a‖) / ↑n) atTop
      (𝓝 (∫ (x : Ω), (fun ω ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
Module: Mathlib.RingTheory.SimpleModule.InjectiveProjective

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : IsSemisimpleRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X Y : Type u_2
x✝⁴ : AddCommGroup X
x✝³ : AddCommGroup Y
x✝² : Module R X
x✝¹ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] M
h : Y →ₗ[R] M
comp : h ∘ₗ f = g
x✝ : X
⊢ h (f x✝) = g x✝

Tactic:
by rw [← comp, LinearMap.comp_apply]

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

Goal state before:
pp: k : Type u
G H K : Type v
inst✝¹⁰ : Ring k
inst✝⁹ : TopologicalSpace k
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalGroup H
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : IsTopologicalGroup K
X : TopRep k G
Y : TopRep k H
Z : TopRep k K
φ : H →ₜ* G
f : res (↑φ) X ⟶ Y
i : ℕ
⊢ invariantsResMap (↑φ) (resolutionMap φ f (i + 1)) ≫ Y.homogeneousCochains.d i (i + 1) =
    X.homogeneousCochains.d i (i + 1) ≫ invariantsResMap (↑φ) (resolutionMap φ f (i + 1 + 1))

Tactic:
rw [homogeneousCochains.d_eq, homogeneousCochains.d_eq, ← invariantsResMap_comp,
      resolutionMap_comp_d, invariantsResMap_map_comp]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
this : Fintype G
x : MonoidAlgebra k G
hx : x ∈ ((linearCombination k fun x ↦ 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)).ker
⊢ x = x.coeff.sum fun g r ↦ MonoidAlgebra.single g r - MonoidAlgebra.single 1 r

Tactic:
ext g

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
this : Fintype G
x : MonoidAlgebra k G
hx : x ∈ ((linearCombination k fun x ↦ 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)).ker
g : G
⊢ x.coeff g = (x.coeff.sum fun g r ↦ MonoidAlgebra.single g r - MonoidAlgebra.single 1 r).coeff g
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
x✝ : ↥(↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
x : C(G, ↑X)
hx' : x ∈ (X.resolution'.X 0).ρ.invariants
hx : ⟨x, hx'⟩ ∈ (↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
⊢ (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨⟨ContinuousMap.const G x, ⋯⟩, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨σ, hσ⟩ => ⟨↑σ 1, ⋯⟩)
        ⟨⟨x, hx'⟩, hx⟩) =
    ⟨⟨x, hx'⟩, hx⟩

Tactic:
ext g

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
x✝ : ↥(↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
x : C(G, ↑X)
hx' : x ∈ (X.resolution'.X 0).ρ.invariants
hx : ⟨x, hx'⟩ ∈ (↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
g : G
⊢ ↑↑((fun x ↦
              match x with
              | ⟨x, hx⟩ => ⟨⟨ContinuousMap.const G x, ⋯⟩, ⋯⟩)
            ((fun x ↦
                match x with
                | ⟨σ, hσ⟩ => ⟨↑σ 1, ⋯⟩)
              ⟨⟨x, hx'⟩, hx⟩))
      g =
    ↑↑⟨⟨x, hx'⟩, hx⟩ g
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
g : Gal(L/K)
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
x✝ : L
hx✝ : (Algebra.norm K) x✝ = 1
x : L
hx : (Algebra.norm K) x = 1
xu : Lˣ := ⋯.unit
hx' : (algebraMap K L) ((Algebra.norm K) ↑xu) = (algebraMap K L) 1
⊢ ∃ y, g ↑y / ↑y = x

Tactic:
← norm_ofAlgebraAutOnUnits_eq xu,

Goal state after:
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
g : Gal(L/K)
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
x✝ : L
hx✝ : (Algebra.norm K) x✝ = 1
x : L
hx : (Algebra.norm K) x = 1
xu : Lˣ := ⋯.unit
hx' : ↑(toMul (toAdditive ((Hom.hom (ofAlgebraAutOnUnits K L).norm) (toAdditive.symm (ofMul xu))))) = (algebraMap K L) 1
⊢ ∃ y, g ↑y / ↑y = x
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝ : Module.IsTorsionFree A L
this : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) g) ε = ε

Tactic:
obtain ⟨ε, hε⟩ := exists_div_of_norm_eq_one hg hη

Goal state after:
K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝ : Module.IsTorsionFree A L
this : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : Lˣ
hε : ↑ε / g ↑ε = (algebraMap B L) η
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) g) ε = ε
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥X.X₃.ρ.invariants
y : ↑X.X₂
hy : (Rep.Hom.hom X.g) y = ↑z
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
⊢ ⇑(Rep.Hom.hom X.f) ∘ (ConcreteCategory.hom (cochainsIso₁ X.X₁).inv) x =
    (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d 0 (0 + 1))) ((ConcreteCategory.hom (cochainsIso₀ X.X₂).inv) y)

Tactic:
ext g

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥X.X₃.ρ.invariants
y : ↑X.X₂
hy : (Rep.Hom.hom X.g) y = ↑z
x : G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₀₁ X.X₂)) y
g : Fin (0 + 1) → G
⊢ (⇑(Rep.Hom.hom X.f) ∘ (ConcreteCategory.hom (cochainsIso₁ X.X₁).inv) x) g =
    (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d 0 (0 + 1))) ((ConcreteCategory.hom (cochainsIso₀ X.X₂).inv) y)
      g
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → ↑X.X₂
hy : ⇑(Rep.Hom.hom X.g) ∘ y = ⇑z
x : G × G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₁₂ X.X₂)) y
⊢ ⇑(Rep.Hom.hom X.f) ∘ (ConcreteCategory.hom (cochainsIso₂ X.X₁).inv) x =
    (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d 1 (1 + 1))) ((ConcreteCategory.hom (cochainsIso₁ X.X₂).inv) y)

Tactic:
ext g

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cocycles₁ X.X₃)
y : G → ↑X.X₂
hy : ⇑(Rep.Hom.hom X.g) ∘ y = ⇑z
x : G × G → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom (d₁₂ X.X₂)) y
g : Fin (1 + 1) → G
⊢ (⇑(Rep.Hom.hom X.f) ∘ (ConcreteCategory.hom (cochainsIso₂ X.X₁).inv) x) g =
    (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d 1 (1 + 1))) ((ConcreteCategory.hom (cochainsIso₁ X.X₂).inv) y)
      g
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥A.ρ.invariants
⊢ (ConcreteCategory.hom (inhomogeneousCochains.d A 0)) ((ConcreteCategory.hom (cochainsIso₀ A).inv) ↑x) = 0

Tactic:
ext g

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥A.ρ.invariants
g : Fin (0 + 1) → G
⊢ (ConcreteCategory.hom (inhomogeneousCochains.d A 0)) ((ConcreteCategory.hom (cochainsIso₀ A).inv) ↑x) g = 0 g