mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: case refine_3
Ω : 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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ ↑i
h_int : Integrable ({ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n ↦ f n) τ)) μ
⊢ ∀ x ∉ {ω | τ ω ≤ σ ω}, {ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n ↦ f n) τ) x = 0

Tactic:
intro x

Goal state after:
case refine_3
Ω : 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
i : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hσ : IsStoppingTime ℱ σ
inst✝ : SigmaFinite (μ.trim ⋯)
hτ_le : ∀ (x : Ω), τ x ≤ ↑i
h_int : Integrable ({ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n ↦ f n) τ)) μ
x : Ω
⊢ x ∉ {ω | τ ω ≤ σ ω} → {ω | τ ω ≤ σ ω}.indicator (stoppedValue (fun n ↦ f n) τ) x = 0
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
⊢ g ⟂ᵢ[k, hk; μ] f ↔
    ⇑(condDistrib f (fun ω ↦ (k ω, g ω)) μ) =ᵐ[Measure.map (fun ω ↦ (k ω, g ω)) μ]
      ⇑(Kernel.prodMkRight β' (condDistrib f k μ))

Tactic:
condDistrib_ae_eq_iff_measure_eq_compProd (μ := μ) _ hf.aemeasurable,

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
⊢ g ⟂ᵢ[k, hk; μ] f ↔
    Measure.map (fun x ↦ ((k x, g x), f x)) μ =
      Measure.map (fun ω ↦ (k ω, g ω)) μ ⊗ₘ Kernel.prodMkRight β' (condDistrib f k μ)
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case h
Ω : 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 ≤ ↑(i + 1)
⊢ ∀ x ∈ Set.Ioc ↑i ↑(i + 1), (↑i + 1) * 1 ≤ x + 1

Tactic:
intro x

Goal state after:
case h
Ω : 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 : ℕ
a✝ : i ∈ range N
I : ↑i ≤ ↑(i + 1)
x : ℝ
⊢ x ∈ Set.Ioc ↑i ↑(i + 1) → (↑i + 1) * 1 ≤ x + 1
Module: Mathlib.Probability.Moments.SubGaussian

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

Tactic:
by
  have : IsProbabilityMeasure μ := h_indep.isProbabilityMeasure
  classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s his h =>
    simp_rw [← Finset.sum_apply, Finset.sum_insert his, Pi.add_apply, Finset.sum_apply]
    have h_indep' := (h_indep.indepFun_finsetSum_of_notMem₀ h_meas his).symm
    refine add_of_indepFun (h_subG _ (Finset.mem_insert_self _ _)) (h ?_) ?_
    · exact fun i hi ↦ h_subG _ (Finset.mem_insert_of_mem hi)
    · convert! h_indep'
      rw [Finset.sum_apply]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
⊢ Tendsto (fun i ↦ ∫ (a : Ω), truncation (X i) (↑i) a) atTop (𝓝 (∫ (a : Ω), X 0 a))

Tactic:
convert! (tendsto_integral_truncation hint).comp tendsto_natCast_atTop_atTop using 1

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
⊢ (fun i ↦ ∫ (a : Ω), truncation (X i) (↑i) a) = (fun A ↦ ∫ (x : Ω), truncation (X 0) A x) ∘ Nat.cast
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e'_7
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
A : Tendsto (fun i ↦ ∫ (a : Ω), truncation (X i) (↑i) a) atTop (𝓝 (∫ (a : Ω), X 0 a))
⊢ (fun n ↦ (∫ (a : Ω), (∑ i ∈ range n, truncation (X i) ↑i) a) - ↑n * ∫ (a : Ω), X 0 a) = fun n ↦
    ∑ i ∈ range n, ((∫ (a : Ω), truncation (X i) (↑i) a) - ∫ (a : Ω), X 0 a)

Tactic:
ext1 n

Goal state after:
case e'_7
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
A : Tendsto (fun i ↦ ∫ (a : Ω), truncation (X i) (↑i) a) atTop (𝓝 (∫ (a : Ω), X 0 a))
n : ℕ
⊢ (∫ (a : Ω), (∑ i ∈ range n, truncation (X i) ↑i) a) - ↑n * ∫ (a : Ω), X 0 a =
    ∑ i ∈ range n, ((∫ (a : Ω), truncation (X i) (↑i) a) - ∫ (a : Ω), X 0 a)
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e'_7
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ω : Ω
hω :
  (fun n ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω -
        ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a) =o[atTop]
    fun n ↦ ↑⌊c ^ n⌋₊
A : Tendsto (fun n ↦ ⌊c ^ n⌋₊) atTop atTop
⊢ (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) = fun x ↦
    (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) ↑i) a) +
      ((fun n ↦ (∫ (a : Ω), (∑ i ∈ range n, truncation (X i) ↑i) a) - ↑n * ∫ (a : Ω), X 0 a) ∘ fun n ↦ ⌊c ^ n⌋₊) x

Tactic:
ext1 n

Goal state after:
case e'_7
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ω : Ω
hω :
  (fun n ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω -
        ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a) =o[atTop]
    fun n ↦ ↑⌊c ^ n⌋₊
A : Tendsto (fun n ↦ ⌊c ^ n⌋₊) atTop atTop
n : ℕ
⊢ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a =
    (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a) +
      ((fun n ↦ (∫ (a : Ω), (∑ i ∈ range n, truncation (X i) ↑i) a) - ↑n * ∫ (a : Ω), X 0 a) ∘ fun n ↦ ⌊c ^ n⌋₊) n
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: case refine_2
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
σ : Representation k G W
f : V →ₗ[k] W
hf : ρ.IsIntertwiningMap σ f
γ : G
⊢ σ γ ∘ₗ f ∘ₗ ρ γ⁻¹ = f

Tactic:
· ext v
    simp [hf.isIntertwining]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e'_7
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊
ω : Ω
hω : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
h'ω : (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n
A : Tendsto (fun n ↦ ⌊c ^ n⌋₊) atTop atTop
⊢ (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) = fun x ↦
    (∑ i ∈ range ⌊c ^ x⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ x⌋₊ * ∫ (a : Ω), X 0 a) -
      ((fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) ∘ fun n ↦ ⌊c ^ n⌋₊) x

Tactic:
ext1 n

Goal state after:
case e'_7
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊
ω : Ω
hω : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
h'ω : (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n
A : Tendsto (fun n ↦ ⌊c ^ n⌋₊) atTop atTop
n : ℕ
⊢ ∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a =
    (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) -
      ((fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) ∘ fun n ↦ ⌊c ^ n⌋₊) n
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e'_7
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊
ω : Ω
hω : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
h'ω : (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n
L : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
⊢ (fun x ↦ (∑ i ∈ range ⌊c ^ x⌋₊, X i ω) / ↑⌊c ^ x⌋₊ - ∫ (a : Ω), X 0 a) = fun x ↦
    (∑ i ∈ range ⌊c ^ x⌋₊, X i ω - ↑⌊c ^ x⌋₊ * ∫ (a : Ω), X 0 a) * (↑⌊c ^ x⌋₊)⁻¹

Tactic:
ext1 n

Goal state after:
case e'_7
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊
ω : Ω
hω : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
h'ω : (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n
L : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
n : ℕ
⊢ (∑ i ∈ range ⌊c ^ n⌋₊, X i ω) / ↑⌊c ^ n⌋₊ - ∫ (a : Ω), X 0 a =
    (∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) * (↑⌊c ^ n⌋₊)⁻¹
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e'_8
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊
ω : Ω
hω : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
h'ω : (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n
L : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
⊢ (fun _x ↦ 1) = fun x ↦ ↑⌊c ^ x⌋₊ * (↑⌊c ^ x⌋₊)⁻¹

Tactic:
ext1 n

Goal state after:
case e'_8
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊
ω : Ω
hω : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
h'ω : (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n
L : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
n : ℕ
⊢ 1 = ↑⌊c ^ n⌋₊ * (↑⌊c ^ n⌋₊)⁻¹
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℕ → ℝ
cone : ∀ (n : ℕ), 1 < c n
clim : Tendsto c atTop (𝓝 1)
this :
  ∀ (k : ℕ), ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) / ↑⌊c k ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
ω : Ω
hω : ∀ (i : ℕ), Tendsto (fun n ↦ (∑ i ∈ range ⌊c i ^ n⌋₊, X i ω) / ↑⌊c i ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
⊢ Monotone fun n ↦ ∑ i ∈ range n, X i ω

pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℕ → ℝ
cone : ∀ (n : ℕ), 1 < c n
clim : Tendsto c atTop (𝓝 1)
this :
  ∀ (k : ℕ), ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) / ↑⌊c k ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
ω : Ω
hω : ∀ (i : ℕ), Tendsto (fun n ↦ (∑ i ∈ range ⌊c i ^ n⌋₊, X i ω) / ↑⌊c i ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
⊢ ∀ (k : ℕ), Tendsto (fun n ↦ (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) / ↑⌊c k ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))

Tactic:
· intro m n hmn
    exact sum_le_sum_of_subset_of_nonneg (range_mono hmn) fun i _ _ => hnonneg i ω

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℕ → ℝ
cone : ∀ (n : ℕ), 1 < c n
clim : Tendsto c atTop (𝓝 1)
this :
  ∀ (k : ℕ), ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) / ↑⌊c k ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
ω : Ω
hω : ∀ (i : ℕ), Tendsto (fun n ↦ (∑ i ∈ range ⌊c i ^ n⌋₊, X i ω) / ↑⌊c i ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
⊢ ∀ (k : ℕ), Tendsto (fun n ↦ (∑ i ∈ range ⌊c k ^ n⌋₊, X i ω) / ↑⌊c k ^ n⌋₊) atTop (𝓝 (∫ (a : Ω), X 0 a))
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
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
have : Nonempty s := ⟨0, zero_s⟩

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
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 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:
← comp,

Goal state after:
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✝) = (h ∘ₗ f) x✝
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁹ : Monoid G
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalAddGroup V
inst✝⁴ : Module R V
inst✝³ : AddCommGroup W
inst✝² : TopologicalSpace W
inst✝¹ : IsTopologicalAddGroup W
inst✝ : Module R W
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
φ ψ : σ.Equiv ρ
h : φ.toContinuousLinearEquiv = ψ.toContinuousLinearEquiv
⊢ φ = ψ

Tactic:
cases φ; cases ψ; simpa [ContIntertwiningMap.ext_iff] using h

Goal state after:
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: case mpr
k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Group G
inst✝² : IsAlgClosed k
inst✝¹ : CharZero k
inst✝ : Fintype G
V : FDRep k G
this : Invertible ↑(Nat.card G)
h : ∑ g, V.character g * V.character g⁻¹ = ↑(Nat.card G)
eq : 1 = ↑(Module.finrank k (V ⟶ V))
⊢ Simple V

Tactic:
rw [simple_iff_end_is_rank_one, ← Nat.cast_inj (R := k), ← eq, Nat.cast_one]

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case hx
k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
a : ↑A
⊢ Function.support
      ↑(A.indToCoind
          ((Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
            ((MonoidAlgebra.lsingle g) 1 ⊗ₜ[k] a))) ⊆
    MulAction.orbit (↥S) g

Tactic:
intro x

Goal state after:
case hx
k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
a : ↑A
x : G
⊢ x ∈
      Function.support
        ↑(A.indToCoind
            ((Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) A.ρ))
              ((MonoidAlgebra.lsingle g) 1 ⊗ₜ[k] a))) →
    x ∈ MulAction.orbit (↥S) g
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
x : ↑(leftRegular k G)
hx : x ∈ (Hom.hom ((leftRegular k G).applyAsHom g - 𝟙 (leftRegular k G))).ker
γ : G
⊢ ((Hom.hom (leftRegular k G).norm).toLinearMap (MonoidAlgebra.single 1 (x.coeff g))).coeff γ = x.coeff γ

Tactic:
have := coeff_of_leftRegular_of_generator (k := k) g hg x
      (by simpa [sub_hom, sub_eq_zero] using! hx) γ

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
x : ↑(leftRegular k G)
hx : x ∈ (Hom.hom ((leftRegular k G).applyAsHom g - 𝟙 (leftRegular k G))).ker
γ : G
this : x.coeff γ = x.coeff g
⊢ ((Hom.hom (leftRegular k G).norm).toLinearMap (MonoidAlgebra.single 1 (x.coeff g))).coeff γ = x.coeff γ
Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
X✝ Y✝ : Rep k G
f : X✝ ⟶ Y✝
⊢ ∀ (i j : ℕ),
    (ComplexShape.down ℕ).Rel i j →
      f ≫ (HomologicalComplex.alternatingConst Y✝ ⋯ ⋯ ⋯).d i j =
        (HomologicalComplex.alternatingConst X✝ ⋯ ⋯ ⋯).d i j ≫ f

Tactic:
rintro i j ⟨rfl⟩
      by_cases hj : Even (j + 1)
      · simp [if_pos hj, norm_comm]
      · simp [if_neg hj, applyAsHom_comm]

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

Goal state before:
pp: case zero.right
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ Function.Surjective
    ⇑(Hom.hom
        ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).map
            ((((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv (trivial k G k)).symm
              ⟨(trivial k G k).leftRegularHom 1, ⋯⟩)).τ₂)

Tactic:
intro x

Goal state after:
case zero.right
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
x :
  ↑((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
        ((ChainComplex.single₀ (Rep k G)).obj (trivial k G k))).X₂
⊢ ∃ a,
    (Hom.hom
          ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).map
              ((((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv (trivial k G k)).symm
                ⟨(trivial k G k).leftRegularHom 1, ⋯⟩)).τ₂)
        a =
      x
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
X Y : Rep k H
f : X ⟶ Y
⊢ ((coinvariantsTensor k H).obj (ind φ A)).map f ≫ (coinvariantsTensorIndIso φ A Y).hom =
    (coinvariantsTensorIndIso φ A X).hom ≫ (resFunctor φ ⋙ (coinvariantsTensor k G).obj A).map f

Tactic:
ext
    simp [coinvariantsTensorIndHom, coinvariantsTensorMk, hom_comm_apply]

Goal state after:
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), (Algebra.norm K) x = 1 → ∃ y, g ↑y / ↑y = x

Tactic:
intro x

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
⊢ (Algebra.norm K) x = 1 → ∃ y, g ↑y / ↑y = x
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : Monoid G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G → M
hf : IsMulCocycle₁ f
⊢ f 1 = 1

Tactic:
simpa only [mul_one, one_smul, left_eq_mul] using hf 1 1

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
⊢ (cocyclesIso₀ A).hom ≫ (shortComplexH0 A).f = iCocycles A 0 ≫ (cochainsIso₀ A).hom

Tactic:
dsimp [cocyclesIso₀]
  apply KernelFork.mapOfIsLimit_ι

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₁ f₂ : G →* H
h : f₁ = f₂
φ : res f₁ A ⟶ B
T : Type u_1
F : (f : G →* H) → (res f A ⟶ B) → T
⊢ F f₁ φ = F f₂ (h ▸ φ)

Tactic:
by
  subst h
  rfl

Goal state after: