mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
μ : (i : ι) → Measure (𝓧 i)
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
hm : AEMeasurable (fun ω i ↦ X i ω) P
h : HasLaw (fun ω i ↦ X i ω) (infinitePi μ) P
⊢ iIndepFun X P

Tactic:
by
    rw [iIndepFun_iff_map_fun_eq_infinitePi_map₀ hm, h.map_eq]
    simp_rw [fun i ↦ (hX i).map_eq]

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

Goal state before:
pp: case neg.refine_2.inr.inl.ha
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
t : Set Ω
ht : MeasurableSet t
h : t = s
⊢ μ.real s ≠ 0

Tactic:
exact ENNReal.toReal_ne_zero.2 ⟨hμs, measure_ne_top _ _⟩

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs2_eq : ∀ s ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
⊢ (∀ (t1 t2 : Set Ω),
      t1 ∈ s1 →
        t2 ∈ s2 →
          ∀ᵐ (a : Ω) ∂μ.trim hm',
            ((condExpKernel μ m') a) (t1 ∩ t2) = ((condExpKernel μ m') a) t1 * ((condExpKernel μ m') a) t2) ↔
    ∀ (t1 t2 : Set Ω),
      t1 ∈ s1 →
        t2 ∈ s2 →
          μ[(t1 ∩ t2).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[t1.indicator fun ω ↦ 1 | m'] * μ[t2.indicator fun ω ↦ 1 | m']

Tactic:
have hs12_eq : ∀ s ∈ s1, ∀ t ∈ s2, (fun ω ↦ ENNReal.toReal (condExpKernel μ m' ω (s ∩ t)))
      =ᵐ[μ] μ⟦s ∩ t | m'⟧ :=
    fun s hs t ht ↦ condExpKernel_ae_eq_condExp hm' ((hs1 s hs).inter ((hs2 t ht)))

Goal state after:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs2_eq : ∀ s ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1, ∀ t ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) (s ∩ t)).toReal) =ᵐ[μ] μ[(s ∩ t).indicator fun ω ↦ 1 | m']
⊢ (∀ (t1 t2 : Set Ω),
      t1 ∈ s1 →
        t2 ∈ s2 →
          ∀ᵐ (a : Ω) ∂μ.trim hm',
            ((condExpKernel μ m') a) (t1 ∩ t2) = ((condExpKernel μ m') a) t1 * ((condExpKernel μ m') a) t2) ↔
    ∀ (t1 t2 : Set Ω),
      t1 ∈ s1 →
        t2 ∈ s2 →
          μ[(t1 ∩ t2).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[t1.indicator fun ω ↦ 1 | m'] * μ[t2.indicator fun ω ↦ 1 | m']
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : Type u_3
γ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : Ω → β
g : Ω → γ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ CondIndepFun m' hm' f g μ ↔ CondIndep m' (MeasurableSpace.comap f mβ) (MeasurableSpace.comap g mγ) hm' μ

Tactic:
by
  simp only [CondIndepFun, CondIndep, Kernel.IndepFun]

Goal state after:
Module: Mathlib.Probability.Martingale.OptionalSampling

Goal state before:
pp: case neg
Ω : 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 : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
inst✝ : SigmaFinite (μ.trim ⋯)
i : ι
hin : ¬i ≤ n
⊢ {x | τ x = ↑i} = ∅

Tactic:
ext1 x

Goal state after:
case neg
Ω : 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 : ι
h : Martingale f ℱ μ
hτ : IsStoppingTime ℱ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
inst✝ : SigmaFinite (μ.trim ⋯)
i : ι
hin : ¬i ≤ n
x : Ω
⊢ x ∈ {x | τ x = ↑i} ↔ x ∈ ∅
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
h_countable_range : (Set.range τ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
⊢ Set.univ = ⋃ i ∈ Set.range τ, {x | τ x = i}

Tactic:
ext1 x

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
h_countable_range : (Set.range τ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
x : Ω
⊢ x ∈ Set.univ ↔ x ∈ ⋃ i ∈ Set.range τ, {x | τ x = i}
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σ : IsStoppingTime ℱ σ
hσ_le_τ : σ ≤ τ
hτ_le : ∀ (x : Ω), τ x ≤ ↑n
hτ_countable_range : (Set.range τ).Countable
hσ_countable_range : (Set.range σ).Countable
inst✝ : SigmaFinite (μ.trim ⋯)
⊢ stoppedValue f σ =ᵐ[μ] μ[stoppedValue f τ | hσ.measurableSpace]

Tactic:
have : SigmaFinite (μ.trim (hτ.measurableSpace_le_of_le hτ_le)) :=
    sigmaFiniteTrim_mono _ (IsStoppingTime.measurableSpace_mono hσ hτ hσ_le_τ)
  have : μ[stoppedValue f τ | hσ.measurableSpace] =ᵐ[μ]
      μ[μ[f n | hτ.measurableSpace] | hσ.measurableSpace] := condExp_congr_ae
    (h.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range hτ hτ_le hτ_countable_range)
  refine (Filter.EventuallyEq.trans ?_
    (condExp_condExp_of_le ?_ (hτ.measurableSpace_le_of_le hτ_le)).symm).trans this.symm
  · exact h.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range hσ
      (fun x => (hσ_le_τ x).trans (hτ_le x)) hσ_countable_range
  · exact hσ.measurableSpace_mono hτ hσ_le_τ

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
⊢ (μ.tilted fun x ↦ t * X x) s = ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ

Tactic:
rw [tilted_apply' _ _ hs, mgf]

Goal state after:
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
inst✝⁴ : TopologicalSpace G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
inst✝¹ : HasOuterApproxClosed G
Z : Ω → G
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mZ : AEMeasurable Z P
h : ∀ (f : G →ᵇ ℝ), ∫ (ω : Ω) in A, f (Z ω) ∂P = P.real A * ∫ (ω : Ω), f (Z ω) ∂P
f : Unit → G →ᵇ ℝ
⊢ ∫ (ω : Ω) in A, ∏ s, (f s) (Z ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (Z ω) ∂P

Tactic:
convert! h (f ())

Goal state after:
case e'_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
inst✝⁴ : TopologicalSpace G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
inst✝¹ : HasOuterApproxClosed G
Z : Ω → G
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mZ : AEMeasurable Z P
h : ∀ (f : G →ᵇ ℝ), ∫ (ω : Ω) in A, f (Z ω) ∂P = P.real A * ∫ (ω : Ω), f (Z ω) ∂P
f : Unit → G →ᵇ ℝ
x✝ : Ω
⊢ ∏ s, (f s) (Z x✝) = (f ()) (Z x✝)

case e'_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
inst✝⁴ : TopologicalSpace G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
inst✝¹ : HasOuterApproxClosed G
Z : Ω → G
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mZ : AEMeasurable Z P
h : ∀ (f : G →ᵇ ℝ), ∫ (ω : Ω) in A, f (Z ω) ∂P = P.real A * ∫ (ω : Ω), f (Z ω) ∂P
f : Unit → G →ᵇ ℝ
x✝ : Ω
⊢ ∏ s, (f s) (Z x✝) = (f ()) (Z x✝)
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : ConditionallyCompleteLinearOrderBot ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝¹ : SecondCountableTopology ι
inst✝ : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
⊢ ∃ nk T, StrictMono nk ∧ Tendsto T atTop atTop ∧ ∀ (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n

Tactic:
by
  obtain ⟨T, hT, h⟩ := isPreLocalizingSequence_of_isLocalizingSequence_aux' hτ hσ
  choose nk hnk using h
  refine ⟨mkStrictMonoAux nk, T, mkStrictMonoAux_strictMono nk, hT,
    fun n ↦ le_trans (EventuallyLE.measure_le ?_) (hnk n)⟩
  filter_upwards [(hσ n).mono] with ω hω
  specialize hω (le_mkStrictMonoAux nk n)
  simp [Set.ofPred]
  grind

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
⊢ {ω | X ω ∈ Set.Ioi ↑i} ⊆ ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}

Tactic:
intro ω hω
        obtain ⟨N, hN⟩ : ∃ N : ℕ, X ω ≤ N := exists_nat_ge (X ω)
        exact Set.mem_iUnion.2 ⟨N, hω, hN⟩

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

Goal state before:
pp: A : Type u_1
V : Type u_2
k : Type u_3
inst✝⁹ : Field k
inst✝⁸ : Ring A
inst✝⁷ : Algebra k A
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module k V
inst✝⁴ : Module A V
inst✝³ : IsScalarTower k A V
inst✝² : IsSimpleModule A V
inst✝¹ : FiniteDimensional k V
inst✝ : IsAlgClosed k
this : Module.Finite k (Module.End A V)
⊢ Function.Bijective ⇑(algebraMap k (Module.End A V))

Tactic:
exact IsAlgClosed.algebraMap_bijective_of_isIntegral (k := k)

Goal state after:
Module: Mathlib.RepresentationTheory.Equiv

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

Tactic:
simp [finsuppTensorLeft, TensorProduct.finsuppLeft_apply_tmul]

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

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hm : m ≤ mΩ
hXm : Measurable X
hX : HasSubgaussianMGF X c μ
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * X ω)) (μ.trim hm)

Tactic:
refine (hX.integrable_exp_mul t).trim hm ?_

Goal state after:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hm : m ≤ mΩ
hXm : Measurable X
hX : HasSubgaussianMGF X c μ
t : ℝ
⊢ StronglyMeasurable fun ω ↦ rexp (t * X ω)
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 : ↥(Representation.coindV φ A.ρ)
g : G
⊢ (linearCombination k ↑f ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ (MonoidHom.comp (leftRegular k H).ρ φ) g =
    A.ρ g ∘ₗ linearCombination k ↑f ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)

Tactic:
by dsimp; ext; simp [f.2 g]

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
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
S : Type u_6
inst✝⁴ : Monoid S
inst✝³ : DistribMulAction S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : LinearMap.CompatibleSMul W W S R
s : S
f : π₁ →ⁱL π₂
g : G
⊢ (s • f.toContinuousLinearMap) ∘SL π₁ g = π₂ g ∘SL (s • f.toContinuousLinearMap)

Tactic:
ContinuousLinearMap.smul_comp,

Goal state after:
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
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
S : Type u_6
inst✝⁴ : Monoid S
inst✝³ : DistribMulAction S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : LinearMap.CompatibleSMul W W S R
s : S
f : π₁ →ⁱL π₂
g : G
⊢ s • f.toContinuousLinearMap ∘SL π₁ g = π₂ g ∘SL (s • f.toContinuousLinearMap)
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
π₂ : ContRepresentation R G W
π₃ : ContRepresentation R G U
S : Type u_6
inst✝⁴ : Monoid S
inst✝³ : DistribMulAction S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : LinearMap.CompatibleSMul W W S R
x✝² : S
x✝¹ x✝ : π₁ →ⁱL π₂
⊢ x✝² • (x✝¹ + x✝) = x✝² • x✝¹ + x✝² • x✝

Tactic:
by ext; simp [smul_add]

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
⊢ Coinvariants.ker (leftRegular k G) = ((linearCombination k fun x ↦ 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)).ker

Tactic:
by
  have := Fintype.ofFinite G
  refine le_antisymm (Submodule.span_le.2 ?_) fun x hx => ?_
  · rintro x ⟨⟨g, y⟩, rfl⟩
    simpa [linearCombination, sub_eq_zero, sum_fintype]
      using Finset.sum_bijective _ (Group.mulLeft_bijective g⁻¹) (by simp) (by lia)
  · have : x = x.coeff.sum (fun g r => .single g r - .single 1 r) := by
      ext g
      by_cases hg : g = 1
      · simp_all [linearCombination, sum_apply', MonoidAlgebra.coeff_finsuppSum]
      · simp_all [sum_apply', MonoidAlgebra.coeff_finsuppSum]
    rw [this]
    exact Submodule.finsuppSum_mem _ _ _ _ fun g _ =>
      Coinvariants.mem_ker_of_eq g (.single 1 (x.coeff g)) _ (by simp)

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
f : k[Fin (n + 1 + 1) → G]
⊢ (Hom.hom ((standardComplex k G).d (n + 1) n)) f = (d k G (n + 1)) f

Tactic:
← Representation.IntertwiningMap.toLinearMap_apply,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
f : k[Fin (n + 1 + 1) → G]
⊢ (Hom.hom ((standardComplex k G).d (n + 1) n)).toLinearMap f = (d k G (n + 1)) f
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

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

Tactic:
by
  have := ((mem_cocycles₂_iff f).1 f.2 1 1 g).symm
  simpa only [map_one, Module.End.one_apply, one_mul, add_right_inj, this]

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
C : ↑(H0 A) → Prop
x : ↑(H0 A)
h : ∀ (x : ↥A.ρ.invariants), C ((ConcreteCategory.hom (H0Iso A).inv) x)
⊢ C x

Tactic:
simpa using h ((H0Iso A).hom x)

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
φ : res 1 A ⟶ B
⊢ mapCocycles₁ 1 φ = 0

Tactic:
rw [← cancel_mono (moduleCatLeftHomologyData (shortComplexH1 B)).i, cyclesMap'_i]
  refine ModuleCat.hom_ext (LinearMap.ext fun _ ↦ funext fun y => ?_)
  simp [mapShortComplexH1, shortComplexH1, Pi.zero_apply y]

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
t : τ
h : t ∉ Set.range ⇑e
⊢ ¬↑{t} ⊆ Set.range ⇑e

Tactic:
Finset.coe_singleton,

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
t : τ
h : t ∉ Set.range ⇑e
⊢ ¬{t} ⊆ Set.range ⇑e
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑(ModuleCat.of k (G × G →₀ ↑A))
⊢ (ModuleCat.Hom.hom (d₂₁ A)) x ∈ cycles₁ A

Tactic:
exact d₂₁_apply_mem_cycles₁ x

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑(shortComplexH0 A).X₂
⊢ (ConcreteCategory.hom (shortComplexH0 A).g) x = 0 → ∃ x₁, (ConcreteCategory.hom (shortComplexH0 A).f) x₁ = x

Tactic:
(hx : Coinvariants.mk _ _ = 0)

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑(shortComplexH0 A).X₂
hx : (Coinvariants.mk A.ρ) x = 0
⊢ ∃ x₁, (ConcreteCategory.hom (shortComplexH0 A).f) x₁ = x
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ π A 2 ≫ (H2Iso A).hom = (isoCycles₂ A).hom ≫ (shortComplexH2 A).moduleCatLeftHomologyData.π

Tactic:
simp [H2Iso, isoCycles₂, π, HomologicalComplex.homologyπ, leftHomologyπ]

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
e : R ≃+* S
this✝ : WithIdeal R := { i := I }
this : WithIdeal S := { i := Ideal.map e I }
⊢ IsHausdorff (Ideal.map e I) S ↔ IsHausdorff I R

Tactic:
rw [iff_comm, IsAdic.isHausdorff_iff rfl, IsAdic.isHausdorff_iff rfl]

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
e : R ≃+* S
this✝ : WithIdeal R := { i := I }
this : WithIdeal S := { i := Ideal.map e I }
⊢ T2Space R ↔ T2Space S
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
a : Option σ
⊢ (optionElim 0 (single i 1)) a = (single (Option.some i) 1) a

Tactic:
cases a

Goal state after:
case none
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
⊢ (optionElim 0 (single i 1)) none = (single (Option.some i) 1) none

case some
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i val✝ : σ
⊢ (optionElim 0 (single i 1)) (Option.some val✝) = (single (Option.some i) 1) (Option.some val✝)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: M : Type u_3
inst✝ : AddCommMonoid M
n : ℕ
i : M
x : Fin n →₀ M
a : Option (Fin n)
⊢ (embDomain (finSuccEquiv n).toEmbedding (Finsupp.cons i x)) a = (optionElim i x) a

Tactic:
cases a

Goal state after:
case none
M : Type u_3
inst✝ : AddCommMonoid M
n : ℕ
i : M
x : Fin n →₀ M
⊢ (embDomain (finSuccEquiv n).toEmbedding (Finsupp.cons i x)) none = (optionElim i x) none

case some
M : Type u_3
inst✝ : AddCommMonoid M
n : ℕ
i : M
x : Fin n →₀ M
val✝ : Fin n
⊢ (embDomain (finSuccEquiv n).toEmbedding (Finsupp.cons i x)) (Option.some val✝) = (optionElim i x) (Option.some val✝)
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
x : AdicCompletion (maximalIdeal R) R
this : (eval (maximalIdeal R) R 1).ker = maximalIdeal R • ⊤
⊢ x ∈ Submodule.restrictScalars R (Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal R)) ↔
    ↑x 1 = 0

Tactic:
← Ideal.smul_top_eq_map

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
x : AdicCompletion (maximalIdeal R) R
this : (eval (maximalIdeal R) R 1).ker = maximalIdeal R • ⊤
⊢ x ∈ maximalIdeal R • ⊤ ↔ ↑x 1 = 0
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
this : IsLocalRing (AdicCompletion (maximalIdeal R) R)
x : IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R)
y : AdicCompletion (maximalIdeal R) R
hy : (residue (AdicCompletion (maximalIdeal R) R)) y = x
z : R
hz : (Ideal.Quotient.mk (maximalIdeal R ^ 1 • ⊤)) z = ↑y 1
⊢ (algebraMap R (AdicCompletion (maximalIdeal R) R)) z - y ∈
    Submodule.restrictScalars R (Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal R))

Tactic:
← Ideal.smul_top_eq_map

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
this : IsLocalRing (AdicCompletion (maximalIdeal R) R)
x : IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R)
y : AdicCompletion (maximalIdeal R) R
hy : (residue (AdicCompletion (maximalIdeal R) R)) y = x
z : R
hz : (Ideal.Quotient.mk (maximalIdeal R ^ 1 • ⊤)) z = ↑y 1
⊢ (algebraMap R (AdicCompletion (maximalIdeal R) R)) z - y ∈ maximalIdeal R • ⊤