mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
r : ℝ≥0
f : ℕ → E
hf : Integrable f Po(r)
⊢ HasSum (fun n ↦ (rexp (-↑r) * ↑r ^ n / ↑n !) • f n) (∫ (n : ℕ), f n ∂Po(r))

Tactic:
have : (fun n ↦ (exp (-r) * r ^ n / (n)!) • f n) =
      fun n ↦ (ENNReal.ofReal (exp (-r) * r ^ n / (n)!)).toReal • f n := by
    ext; rw [ENNReal.toReal_ofReal (by positivity)]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
r : ℝ≥0
f : ℕ → E
hf : Integrable f Po(r)
this : (fun n ↦ (rexp (-↑r) * ↑r ^ n / ↑n !) • f n) = fun n ↦ (ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !)).toReal • f n
⊢ HasSum (fun n ↦ (rexp (-↑r) * ↑r ^ n / ↑n !) • f n) (∫ (n : ℕ), f n ∂Po(r))
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s μ
t : Set Ω
ht_tail : MeasurableSet t
⊢ μ t = 0 ∨ μ t = 1

Tactic:
simpa only [ae_dirac_eq, Filter.eventually_pure]
    using! Kernel.measure_zero_or_one_of_measurableSet_limsup_atBot h_le h_indep ht_tail

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

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

Tactic:
rw [lintegral_add_right, hg₁, hg₂]

Goal state after:
case refine_2.hg
X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
f g : X → ℝ≥0∞
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
hf : Measurable f
hg : Measurable g
x₀ : X
g₁ g₂ : X → ℝ≥0∞
a✝ : Measurable g₁
hg₂_meas : Measurable g₂
hg₁ : ∫⁻ (x : X), g₁ x * f x ∂π x₀ = g₁ x₀ * ∫⁻ (x : X), f x ∂π x₀
hg₂ : ∫⁻ (x : X), g₂ x * f x ∂π x₀ = g₂ x₀ * ∫⁻ (x : X), f x ∂π x₀
⊢ Measurable fun x ↦ g₂ x * f x
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: case mpr
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := ⋯
a : ↑I
h_monotone : ∀ (s : X), Monotone fun x ↦ (κ s).real (Icc 0 x)
e : X × ↑I
⊢ (∃ i, ↑a < ↑i ∧ ∃ (x : 0 ≤ i ∧ ↑i ≤ 1), (κ e.1).real (Icc 0 ⟨↑i, ⋯⟩) < ↑e.2) →
    ∃ a_2, ∃ (h : 0 ≤ a_2 ∧ a_2 ≤ 1), (κ e.1).real (Icc 0 ⟨a_2, ⋯⟩) < ↑e.2 ∧ a < ⟨a_2, ⋯⟩

Tactic:
intro he

Goal state after:
case mpr
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
a : ↑I
h_monotone : ∀ (s : X), Monotone fun x ↦ (κ s).real (Icc 0 x)
e : X × ↑I
he : ∃ i, ↑a < ↑i ∧ ∃ (x : 0 ≤ i ∧ ↑i ≤ 1), (κ e.1).real (Icc 0 ⟨↑i, ⋯⟩) < ↑e.2
⊢ ∃ a_1, ∃ (h : 0 ≤ a_1 ∧ a_1 ≤ 1), (κ e.1).real (Icc 0 ⟨a_1, ⋯⟩) < ↑e.2 ∧ a < ⟨a_1, ⋯⟩
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✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝² : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst✝¹ : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
inst✝ : SigmaFinite (μ.trim ⋯)
i : ι
⊢ stoppedValue f τ =ᵐ[μ.restrict {x | τ x = ↑i}] μ[f n | hτ.measurableSpace]

Tactic:
refine Filter.EventuallyEq.trans ?_
    (condExp_stopping_time_ae_eq_restrict_eq_const_of_le_const h hτ hτ_le i).symm

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✝⁵ : TopologicalSpace ι
inst✝⁴ : OrderTopology ι
inst✝³ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝² : SigmaFiniteFiltration μ ℱ
τ : Ω → WithTop ι
f : ι → Ω → E
n : ι
inst✝¹ : Nonempty ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
inst✝ : SigmaFinite (μ.trim ⋯)
i : ι
⊢ stoppedValue f τ =ᵐ[μ.restrict {x | τ x = ↑i}] f i
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: case refine_1
Ω : 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 ⋯)
⊢ ∀ᵐ (x : Ω) ∂μ.restrict {x | σ x ≤ τ x},
    μ[stoppedValue f τ | ⋯.measurableSpace] x = μ[stoppedValue f τ | hσ.measurableSpace] x

Tactic:
exact condExp_min_stopping_time_ae_eq_restrict_le hσ hτ

Goal state after:
Module: Mathlib.Probability.Process.Kolmogorov

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q 0
s t : T
⊢ ∫⁻ (a : Ω), edist (X s a) (X t a) ^ p ∂P ≤ 0

Tactic:
calc ∫⁻ ω, edist (X s ω) (X t ω) ^ p ∂P
  _ ≤ 0 * edist s t ^ q := hX.kolmogorovCondition s t
  _ = 0 := by simp

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
r : ℝ
ω : Ω'
hω : ∀ (t : ℝ), mgf X (κ ω) t ≤ rexp (↑c * t ^ 2 / 2)
t : ℝ
⊢ ↑c * (t * r) ^ 2 / 2 = ↑(NNReal.mk (r ^ 2) ⋯ * c) * t ^ 2 / 2

Tactic:
simp only [NNReal.coe_mul, NNReal.coe_mk]

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
r : ℝ
ω : Ω'
hω : ∀ (t : ℝ), mgf X (κ ω) t ≤ rexp (↑c * t ^ 2 / 2)
t : ℝ
⊢ ↑c * (t * r) ^ 2 / 2 = r ^ 2 * ↑c * t ^ 2 / 2
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω' : Ω'
h2 : (κ ω') {ω | 0 < X ω} = 0
h1 : (κ ω') {ω | X ω < 0} = 0
⊢ (κ ω') {ω | X ω < 0} + (κ ω') {ω | 0 < X ω} = 0

Tactic:
by simp [h1, h2]

Goal state after:
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : ConditionallyCompleteLinearOrderBot ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst✝⁴ : Zero E
inst✝³ : DenselyOrdered ι
inst✝² : FirstCountableTopology ι
inst✝¹ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
hp : IsStable 𝓕 p
inst✝ : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
hpτ : ∀ (n : ℕ), p (stoppedProcess (fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)) (τ n))
n : ℕ
⊢ p
    (stoppedProcess (fun i ↦ {ω | ⊥ < ⨅ j, ⨅ (_ : j ≥ n), τ j ω}.indicator (stoppedProcess X (fun ω ↦ τ n ω) i)) fun x ↦
      ⨅ j, ⨅ (_ : j ≥ n), τ j x)

Tactic:
convert!
    hp _ (hpτ n) (fun ω ↦ ⨅ j ≥ n, τ j ω) <| hτ.isLocalizingSequence_biInf.isStoppingTime n using 2

Goal state after:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : ConditionallyCompleteLinearOrderBot ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst✝⁴ : Zero E
inst✝³ : DenselyOrdered ι
inst✝² : FirstCountableTopology ι
inst✝¹ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
hp : IsStable 𝓕 p
inst✝ : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
hpτ : ∀ (n : ℕ), p (stoppedProcess (fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)) (τ n))
n : ℕ
⊢ (fun i ↦ {ω | ⊥ < ⨅ j, ⨅ (_ : j ≥ n), τ j ω}.indicator (stoppedProcess X (fun ω ↦ τ n ω) i)) = fun i ↦
    {ω | ⊥ < ⨅ j, ⨅ (_ : j ≥ n), τ j ω}.indicator (stoppedProcess (fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)) (τ n) i)
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 ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
i : ℕ
a✝ : i ∈ range N
I : ↑i ≤ ↑(i + 1)
⊢ (↑i + 1) * ∫ (x : ℝ) in Set.Ioc ↑i ↑(i + 1), 1 ∂ρ ≤ ∫ (x : ℝ) in Set.Ioc ↑i ↑(i + 1), x + 1 ∂ρ

Tactic:
← integral_const_mul

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)
⊢ ∫ (a : ℝ) in Set.Ioc ↑i ↑(i + 1), (↑i + 1) * 1 ∂ρ ≤ ∫ (x : ℝ) in Set.Ioc ↑i ↑(i + 1), x + 1 ∂ρ
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
X Y : Action (Type w) G
f : X ⟶ Y
x : X.V
r : k
⊢ (linearizeMap f) (MonoidAlgebra.single x r) = MonoidAlgebra.single ((ConcreteCategory.hom f.hom) x) r

Tactic:
by
  simp [linearizeMap]

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

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

Tactic:
simp_rw [← Finset.sum_apply, Finset.sum_insert his, Pi.add_apply, Finset.sum_apply]

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

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
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 : ρ.asModule →ₗ[A[G]] σ.asModule
g : G
v : V
⊢ ({ toAddHom := f.toAddHom, map_smul' := ⋯ } ∘ₗ ρ g) v = (σ g ∘ₗ { toAddHom := f.toAddHom, map_smul' := ⋯ }) v

Tactic:
simpa using! f.map_smul' (MonoidAlgebra.single g 1) v

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

Goal state before:
pp: case mp
G : Type v1
H : Type v2
inst✝² : Monoid G
inst✝¹ : Monoid H
k : Type u
inst✝ : CommRing k
φ : H →* G
S : ShortComplex (Rep k G)
⊢ (S.map (resFunctor φ)).ShortExact → S.ShortExact

Tactic:
intro h

Goal state after:
case mp
G : Type v1
H : Type v2
inst✝² : Monoid G
inst✝¹ : Monoid H
k : Type u
inst✝ : CommRing k
φ : H →* G
S : ShortComplex (Rep k G)
h : (S.map (resFunctor φ)).ShortExact
⊢ S.ShortExact
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
⊢ Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹ = f → f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f

Tactic:
intro 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
⊢ f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f
Module: Mathlib.RepresentationTheory.Invariants

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

Tactic:
intro h

Goal state after:
case mpr
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
X Y : Rep k G
f : ↑X →ₗ[k] ↑Y
g : G
h : f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f
⊢ Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹ = f
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: 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

Tactic:
simp [F, Y, ← sum_smul, smul_smul]

Goal state after:
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
U : Type u_5
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
inst✝³ : AddCommGroup U
inst✝² : Module R U
inst✝¹ : TopologicalSpace U
inst✝ : IsTopologicalAddGroup U
π : ContRepresentation R G V
x✝¹ : R
x✝ : V
hv : x✝ ∈ {v | ∀ (g : G), (π g) v = v}
g : G
⊢ (π g) (x✝¹ • x✝) = x✝¹ • x✝

Tactic:
simp [hv g]

Goal state after:
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: case mp
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)
⊢ Simple V → ∑ g, V.character g * V.character g⁻¹ = ↑(Nat.card G)

Tactic:
intro h

Goal state after:
case mp
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 : Simple V
⊢ ∑ g, V.character g * V.character g⁻¹ = ↑(Nat.card G)
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)
⊢ ∑ g, V.character g * V.character g⁻¹ = ↑(Nat.card G) → Simple V

Tactic:
intro h

Goal state after:
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)
⊢ Simple V
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
U : Type u_5
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
inst✝¹³ : AddCommGroup U
inst✝¹² : Module R U
inst✝¹¹ : TopologicalSpace U
inst✝¹⁰ : IsTopologicalAddGroup U
H✝ : Type u_6
inst✝⁹ : Monoid H✝
π✝ : ContRepresentation R G✝ V
π' : ContRepresentation R H✝ W
G : Type u_7
H : Type u_8
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalSpace R
inst✝⁵ : ContinuousSMul R V
inst✝⁴ : ContinuousSMul R W
inst✝³ : Group H
inst✝² : TopologicalSpace H
φ : G →ₜ* H
π : ContRepresentation R G V
inst✝¹ : IsTopologicalGroup G
inst✝ : IsTopologicalGroup H
π₁ : ContRepresentation R G V
π₂ : ContRepresentation R G W
f : π₁ →ⁱL π₂
g : G
⊢ { toFun := (↑f).comp, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } ∘SL π₁.coind₁ g =
    π₂.coind₁ g ∘SL { toFun := (↑f).comp, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

Tactic:
ext; simp [f.isIntertwining]

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

Goal state before:
pp: case succ
k : Type u
G : Type v
inst✝⁴ : Ring k
inst✝³ : TopologicalSpace k
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
i : ℕ
ih : resolutionMap (ContinuousMonoidHom.id G) (𝟙 X) i = 𝟙 (X.resolutionX i)
⊢ resolutionMap (ContinuousMonoidHom.id G) (𝟙 X) (i + 1) = 𝟙 (X.resolutionX (i + 1))

Tactic:
resolutionMap_succ,

Goal state after:
case succ
k : Type u
G : Type v
inst✝⁴ : Ring k
inst✝³ : TopologicalSpace k
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
i : ℕ
ih : resolutionMap (ContinuousMonoidHom.id G) (𝟙 X) i = 𝟙 (X.resolutionX i)
⊢ ofHom (coind₁ResMap (ContinuousMonoidHom.id G) (Hom.hom (resolutionMap (ContinuousMonoidHom.id G) (𝟙 X) i))) =
    𝟙 (X.resolutionX (i + 1))
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality

Goal state before:
pp: case succ
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
ψ : K →ₜ* H
f : res (↑φ) X ⟶ Y
g : res (↑ψ) Y ⟶ Z
i : ℕ
ih :
  resolutionMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) i =
    (resFunctor ↑ψ).map (resolutionMap φ f i) ≫ resolutionMap ψ g i
⊢ resolutionMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) (i + 1) =
    (resFunctor ↑ψ).map (resolutionMap φ f (i + 1)) ≫ resolutionMap ψ g (i + 1)

Tactic:
resolutionMap_succ,

Goal state after:
case succ
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
ψ : K →ₜ* H
f : res (↑φ) X ⟶ Y
g : res (↑ψ) Y ⟶ Z
i : ℕ
ih :
  resolutionMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) i =
    (resFunctor ↑ψ).map (resolutionMap φ f i) ≫ resolutionMap ψ g i
⊢ ofHom (coind₁ResMap (φ.comp ψ) (Hom.hom (resolutionMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) i))) =
    (resFunctor ↑ψ).map (resolutionMap φ f (i + 1)) ≫ resolutionMap ψ g (i + 1)
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality

Goal state before:
pp: case succ
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
ψ : K →ₜ* H
f : res (↑φ) X ⟶ Y
g : res (↑ψ) Y ⟶ Z
i : ℕ
ih :
  resolutionMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) i =
    (resFunctor ↑ψ).map (resolutionMap φ f i) ≫ resolutionMap ψ g i
⊢ ofHom (coind₁ResMap (φ.comp ψ) (Hom.hom (resolutionMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) i))) =
    (resFunctor ↑ψ).map (resolutionMap φ f (i + 1)) ≫ resolutionMap ψ g (i + 1)

Tactic:
resolutionMap_succ,

Goal state after:
case succ
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
ψ : K →ₜ* H
f : res (↑φ) X ⟶ Y
g : res (↑ψ) Y ⟶ Z
i : ℕ
ih :
  resolutionMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) i =
    (resFunctor ↑ψ).map (resolutionMap φ f i) ≫ resolutionMap ψ g i
⊢ ofHom (coind₁ResMap (φ.comp ψ) (Hom.hom (resolutionMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) i))) =
    (resFunctor ↑ψ).map (ofHom (coind₁ResMap φ (Hom.hom (resolutionMap φ f i)))) ≫ resolutionMap ψ g (i + 1)
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality

Goal state before:
pp: case succ
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
ψ : K →ₜ* H
f : res (↑φ) X ⟶ Y
g : res (↑ψ) Y ⟶ Z
i : ℕ
ih :
  resolutionMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) i =
    (resFunctor ↑ψ).map (resolutionMap φ f i) ≫ resolutionMap ψ g i
⊢ ofHom (coind₁ResMap (φ.comp ψ) (Hom.hom (resolutionMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) i))) =
    (resFunctor ↑ψ).map (ofHom (coind₁ResMap φ (Hom.hom (resolutionMap φ f i)))) ≫ resolutionMap ψ g (i + 1)

Tactic:
resolutionMap_succ,

Goal state after:
case succ
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
ψ : K →ₜ* H
f : res (↑φ) X ⟶ Y
g : res (↑ψ) Y ⟶ Z
i : ℕ
ih :
  resolutionMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) i =
    (resFunctor ↑ψ).map (resolutionMap φ f i) ≫ resolutionMap ψ g i
⊢ ofHom (coind₁ResMap (φ.comp ψ) (Hom.hom (resolutionMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) i))) =
    (resFunctor ↑ψ).map (ofHom (coind₁ResMap φ (Hom.hom (resolutionMap φ f i)))) ≫
      ofHom (coind₁ResMap ψ (Hom.hom (resolutionMap ψ g i)))
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality

Goal state before:
pp: case succ
k : Type u
G H : 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
X : TopRep k G
Y : TopRep k H
φ : H →ₜ* G
f : res (↑φ) X ⟶ Y
i : ℕ
ih : resolutionMap φ f i ≫ Y.d i = (resFunctor ↑φ).map (X.d i) ≫ resolutionMap φ f (i + 1)
⊢ resolutionMap φ f (i + 1) ≫ Y.d (i + 1) = (resFunctor ↑φ).map (X.d (i + 1)) ≫ resolutionMap φ f (i + 1 + 1)

Tactic:
ext : 1
    replace ih := congr($(ih).hom)
    simp only [TopRep.hom_comp, resolutionMap_succ, TopRep.hom_ofHom, hom_d_succ,
      ContIntertwiningMap.restrict_sub, ContIntertwiningMap.sub_comp,
      ContIntertwiningMap.comp_sub, coind₁Map_comp_coind₁ResMap,
      coind₁ResMap_comp_coind₁Map_restrict] at ih ⊢
    rw [ih, ← coind₁ResMap_comp_coind₁ι_restrict]

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

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

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

Goal state after: