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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
ι : Type u_3
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝ : Countable ι
E : ι → Type u_6
mE : (i : ι) → MeasurableSpace (E i)
X : (i : ι) → Ω → E i
Y : (i : ι) → Ω' → E i
h : ∀ (i : ι), IdentDistrib (X i) (Y i) μ ν
hX_ind : iIndepFun X μ
hY_ind : iIndepFun Y ν
this✝ : IsProbabilityMeasure μ
this : IsProbabilityMeasure ν
⊢ (Measure.infinitePi fun i ↦ Measure.map (X i) μ) = Measure.map (fun ω x ↦ Y x ω) ν

Tactic:
(iIndepFun_iff_map_fun_eq_infinitePi_map₀' (fun i ↦ (h i).aemeasurable_snd)).mp hY_ind

Goal state after:
Ω : Type u_1
Ω' : Type u_2
ι : Type u_3
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
μ : Measure Ω
ν : Measure Ω'
inst✝ : Countable ι
E : ι → Type u_6
mE : (i : ι) → MeasurableSpace (E i)
X : (i : ι) → Ω → E i
Y : (i : ι) → Ω' → E i
h : ∀ (i : ι), IdentDistrib (X i) (Y i) μ ν
hX_ind : iIndepFun X μ
hY_ind : iIndepFun Y ν
this✝ : IsProbabilityMeasure μ
this : IsProbabilityMeasure ν
⊢ (Measure.infinitePi fun i ↦ Measure.map (X i) μ) = Measure.infinitePi fun i ↦ Measure.map (Y i) ν
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: α : Type u_1
s : Multiset α
hs : s ≠ 0
⊢ ∑' (b : α), ↑(Multiset.count b s) / ↑s.card = (↑s.card)⁻¹ * ∑' (b : α), ↑(Multiset.count b s)

Tactic:
simp_rw [ENNReal.div_eq_inv_mul, ENNReal.tsum_mul_left]

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
inst✝ : IsMarkovKernel κ
π : Measure α
h_rev : κ.IsReversible π
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α), (κ x) s ∂π = ∫⁻ (x : α) in s, (κ x) Set.univ ∂π

Tactic:
by simpa [restrict_univ] using (h_rev hs .univ).symm

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

Goal state before:
pp: a✝¹ : PUnit.{u + 1}
s✝ : Set (PUnit.{u + 1} × PUnit.{u + 1})
a✝ : MeasurableSet s✝
⊢ ((Kernel.copy PUnit.{u + 1}) a✝¹) s✝ = ((Kernel.id.map fun x ↦ (PUnit.unit, x)) a✝¹) s✝

Tactic:
rw [Kernel.id_map (by fun_prop)]

Goal state after:
a✝¹ : PUnit.{u + 1}
s✝ : Set (PUnit.{u + 1} × PUnit.{u + 1})
a✝ : MeasurableSet s✝
⊢ ((Kernel.copy PUnit.{u + 1}) a✝¹) s✝ = ((Kernel.deterministic (fun x ↦ (PUnit.unit, x)) ⋯) a✝¹) s✝
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.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✝⁵ : SecondCountableTopology ι
inst✝⁴ : IsFiniteMeasure P
inst✝³ : DenselyOrdered ι
inst✝² : NoMaxOrder ι
inst✝¹ : Zero E
inst✝ : 𝓕.IsRightContinuous
hp : IsStable 𝓕 p
hL : Locally (fun Y ↦ Locally p 𝓕 Y P) 𝓕 X P
τ : ℕ → ℕ → Ω → WithTop ι
hτ₁ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (τ n) P
hτ₂ :
  ∀ (n n_1 : ℕ),
    p
      (stoppedProcess
        (fun i ↦
          {ω | ⊥ < τ n n_1 ω}.indicator
            (stoppedProcess (fun i ↦ {ω | ⊥ < hL.localSeq n ω}.indicator (X i)) (hL.localSeq n) i))
        (τ n n_1))
nk : ℕ → ℕ
hnk : StrictMono nk
hpre : IsPreLocalizingSequence 𝓕 (fun i ω ↦ min (hL.localSeq i ω) (τ i (nk i) ω)) P
n : ℕ
i : ι
ω : Ω
⊢ (fun i ↦
        {ω | ⊥ < min (hL.localSeq n ω) (τ n (nk n) ω)}.indicator
          (stoppedProcess X (fun ω ↦ min (hL.localSeq n ω) (τ n (nk n) ω)) i))
      i ω =
    (fun i ↦
        {ω | ⊥ < τ n (nk n) ω}.indicator
          ((fun i ↦ {ω | ⊥ < hL.localSeq n ω}.indicator (stoppedProcess X (τ n (nk n) ⊓ hL.localSeq n) i)) i))
      i ω

Tactic:
simp only [lt_inf_iff, Set.indicator_indicator]

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✝⁵ : SecondCountableTopology ι
inst✝⁴ : IsFiniteMeasure P
inst✝³ : DenselyOrdered ι
inst✝² : NoMaxOrder ι
inst✝¹ : Zero E
inst✝ : 𝓕.IsRightContinuous
hp : IsStable 𝓕 p
hL : Locally (fun Y ↦ Locally p 𝓕 Y P) 𝓕 X P
τ : ℕ → ℕ → Ω → WithTop ι
hτ₁ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (τ n) P
hτ₂ :
  ∀ (n n_1 : ℕ),
    p
      (stoppedProcess
        (fun i ↦
          {ω | ⊥ < τ n n_1 ω}.indicator
            (stoppedProcess (fun i ↦ {ω | ⊥ < hL.localSeq n ω}.indicator (X i)) (hL.localSeq n) i))
        (τ n n_1))
nk : ℕ → ℕ
hnk : StrictMono nk
hpre : IsPreLocalizingSequence 𝓕 (fun i ω ↦ min (hL.localSeq i ω) (τ i (nk i) ω)) P
n : ℕ
i : ι
ω : Ω
⊢ {ω | ⊥ < hL.localSeq n ω ∧ ⊥ < τ n (nk n) ω}.indicator
      (stoppedProcess X (fun ω ↦ min (hL.localSeq n ω) (τ n (nk n) ω)) i) ω =
    ({ω | ⊥ < τ n (nk n) ω} ∩ {ω | ⊥ < hL.localSeq n ω}).indicator (stoppedProcess X (τ n (nk n) ⊓ hL.localSeq n) i) ω
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
Y : Ω → ℝ
h' : X =ᵐ[μ] Y
⊢ HasSubgaussianMGF Y c μ

Tactic:
HasSubgaussianMGF_iff_kernel

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())
Y : Ω → ℝ
h' : X =ᵐ[μ] Y
⊢ Kernel.HasSubgaussianMGF Y c (Kernel.const Unit μ) (Measure.dirac ())
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
t : ℝ
p : ℝ≥0
⊢ MemLp (fun ω ↦ rexp (t * X ω)) (↑p) μ

Tactic:
HasSubgaussianMGF_iff_kernel

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())
t : ℝ
p : ℝ≥0
⊢ MemLp (fun ω ↦ rexp (t * X ω)) (↑p) μ
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
t : ℝ
⊢ cgf X μ t ≤ ↑c * t ^ 2 / 2

Tactic:
HasSubgaussianMGF_iff_kernel

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())
t : ℝ
⊢ cgf X μ t ≤ ↑c * t ^ 2 / 2
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
r : ℝ
⊢ HasSubgaussianMGF (fun ω ↦ r * X ω) (⟨r ^ 2, ⋯⟩ * c) μ

Tactic:
HasSubgaussianMGF_iff_kernel

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())
r : ℝ
⊢ Kernel.HasSubgaussianMGF (fun ω ↦ r * X ω) (⟨r ^ 2, ⋯⟩ * c) (Kernel.const Unit μ) (Measure.dirac ())
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
ε : ℝ
hε : 0 ≤ ε
⊢ μ.real {ω | ε ≤ X ω} ≤ rexp (-ε ^ 2 / (2 * ↑c))

Tactic:
HasSubgaussianMGF_iff_kernel

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ())
ε : ℝ
hε : 0 ≤ ε
⊢ μ.real {ω | ε ≤ X ω} ≤ rexp (-ε ^ 2 / (2 * ↑c))
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e_f.e_a.h
Ω : 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
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := fun n ↦ truncation (X n) ↑n
S : ℕ → Ω → ℝ := fun n ↦ ∑ i ∈ range n, Y i
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := fun n ↦ ⌊c ^ n⌋₊
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * ∫ (a : Ω), X 0 a)
N i : ℕ
⊢ (↑(range (u i))).Pairwise fun i j ↦ Y i ⟂ᵢ Y j

Tactic:
· intro k _ l _ hkl
          exact (hindep hkl).comp (A k).measurable (A l).measurable

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

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝¹ : StandardBorelSpace Ω
inst✝ : IsFiniteMeasure μ
Y : Ω → ℝ
cX cY : ℝ≥0
hm : m ≤ mΩ
hX : HasSubgaussianMGF X cX (μ.trim hm)
hY : HasCondSubgaussianMGF m hm Y cY μ
⊢ HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (cX + cY) (Measure.map Function.diag μ)

Tactic:
HasSubgaussianMGF_iff_kernel

Goal state after:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝¹ : StandardBorelSpace Ω
inst✝ : IsFiniteMeasure μ
Y : Ω → ℝ
cX cY : ℝ≥0
hm : m ≤ mΩ
hX : Kernel.HasSubgaussianMGF X cX (Kernel.const Unit (μ.trim hm)) (Measure.dirac ())
hY : HasCondSubgaussianMGF m hm Y cY μ
⊢ Kernel.HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (cX + cY) (Kernel.const Unit (Measure.map Function.diag μ))
    (Measure.dirac ())
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring A
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module A V
ρ : Representation A G V
g : G
hg : g ∈ Submonoid.center G
⊢ ∀ (g_1 : G) (v : V), (ρ g) ((ρ g_1) v) = (ρ g_1) ((ρ g) v)

Tactic:
intro g' v

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring A
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module A V
ρ : Representation A G V
g : G
hg : g ∈ Submonoid.center G
g' : G
v : V
⊢ (ρ g) ((ρ g') v) = (ρ g') ((ρ g) v)
Module: Mathlib.RepresentationTheory.FDRep

Goal state before:
pp: R : Type u
G : Type v
inst✝¹ : CommRing R
inst✝ : Monoid G
V W : FDRep R G
i : V ≅ W
g : G
⊢ W.ρ g =
    ModuleCat.Hom.hom
      (((Action.forget (FGModuleCat R) G).mapIso i).inv ≫ V.ρ g ≫ ((Action.forget (FGModuleCat R) G).mapIso i).hom).hom

Tactic:
← ModuleCat.hom_ofHom (W.ρ g),

Goal state after:
R : Type u
G : Type v
inst✝¹ : CommRing R
inst✝ : Monoid G
V W : FDRep R G
i : V ≅ W
g : G
⊢ ModuleCat.Hom.hom (ModuleCat.ofHom (W.ρ g)) =
    ModuleCat.Hom.hom
      (((Action.forget (FGModuleCat R) G).mapIso i).inv ≫ V.ρ g ≫ ((Action.forget (FGModuleCat R) G).mapIso i).hom).hom
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) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ∞
B : ∀ᵐ (ω : Ω), Tendsto (fun n ↦ truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)
ω : Ω
hω : Tendsto (fun n ↦ truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)
n : ℕ
⊢ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω = ∑ i ∈ range n, (truncation (X i) (↑i) ω - X i ω)

Tactic:
sum_sub_distrib

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) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
A : ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ∞
B : ∀ᵐ (ω : Ω), Tendsto (fun n ↦ truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)
ω : Ω
hω : Tendsto (fun n ↦ truncation (X n) (↑n) ω - X n ω) atTop (𝓝 0)
n : ℕ
⊢ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω =
    ∑ x ∈ range n, truncation (X x) (↑x) ω - ∑ x ∈ range n, X x ω
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: k : Type u
inst✝¹ : Field k
G : Type v
inst✝ : Group G
V W : FDRep k G
g : G
⊢ (of (linHom V.ρ W.ρ)).character g = V.character g⁻¹ * W.character g

Tactic:
rw [← char_iso (dualTensorIsoLinHom _ _), char_tensor, Pi.mul_apply, char_dual]

Goal state after:
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: k : Type u
inst✝⁶ : Field k
G : Type v
inst✝⁵ : Group G
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype G
inst✝² : Invertible ↑(Nat.card G)
V W : FDRep k G
inst✝¹ : Simple V
inst✝ : Simple W
⊢ (↑(Nat.card G))⁻¹ * ∑ g, V.character g * W.character g⁻¹ = if Nonempty (V ≅ W) then 1 else 0

Tactic:
scalar_product_char_eq_finrank_equivariant

Goal state after:
k : Type u
inst✝⁶ : Field k
G : Type v
inst✝⁵ : Group G
inst✝⁴ : IsAlgClosed k
inst✝³ : Fintype G
inst✝² : Invertible ↑(Nat.card G)
V W : FDRep k G
inst✝¹ : Simple V
inst✝ : Simple W
⊢ ↑(finrank k (W ⟶ V)) = if Nonempty (V ≅ W) then 1 else 0
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Basic

Goal state before:
pp: case succ
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
n : ℕ
ih : X.d n ≫ X.d (n + 1) = 0
⊢ X.d (n + 1) ≫ X.d (n + 1 + 1) = 0

Tactic:
d_succ _ (n + 1),

Goal state after:
case succ
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
n : ℕ
ih : X.d n ≫ X.d (n + 1) = 0
⊢ X.d (n + 1) ≫ (ofHom (X.resolutionX (n + 1 + 1)).ρ.coind₁ι - (coind₁Functor k G).map (X.d (n + 1))) = 0
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case inl
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
g₁ : G
a : ↑A
s s₁ : ↥S
⊢ (A.ρ ⟨s₁ • g₁ * (↑s * g₁)⁻¹, ⋯⟩) ((A.ρ s) a) =
    (if h : (QuotientGroup.rightRel S) (s₁ • g₁) g₁ then A.ρ ⟨s₁ • g₁ * g₁⁻¹, ⋯⟩ else 0) a

Tactic:
dif_pos ⟨s₁, rfl⟩,

Goal state after:
case inl
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
g₁ : G
a : ↑A
s s₁ : ↥S
⊢ (A.ρ ⟨s₁ • g₁ * (↑s * g₁)⁻¹, ⋯⟩) ((A.ρ s) a) = (A.ρ ⟨s₁ • g₁ * g₁⁻¹, ⋯⟩) a
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n : ℕ
⊢ d A n =
    (freeLiftLEquiv k G (Fin n → G) A).toModuleIso.inv ≫
      ((barComplex k G).linearYonedaObj k A).d n (n + 1) ≫ (freeLiftLEquiv k G (Fin (n + 1) → G) A).toModuleIso.hom

Tactic:
ext
  simp [d_hom_apply, map_add, barComplex.d_single (k := k), homEquiv]

Goal state after:
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
s : G
x : ↑A
y : ↑B
⊢ (((Representation.ind φ A.ρ).tprod B.ρ) (φ s)) ((IndV.mk φ A.ρ 1) x ⊗ₜ[k] y) - (IndV.mk φ A.ρ 1) x ⊗ₜ[k] y =
    (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ))
          (MonoidAlgebra.single 1 1 ⊗ₜ[k] (A.ρ s) x) ⊗ₜ[k]
        (B.ρ (φ s)) y -
      (Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k H) φ) A.ρ))
          (MonoidAlgebra.single 1 1 ⊗ₜ[k] x) ⊗ₜ[k]
        y

Tactic:
by
      simp [← Coinvariants.mk_inv_tmul]

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

Goal state before:
pp: case neg
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
x : leftRegular k G ⟶ A
hi : ¬Even i
⊢ (ModuleCat.Hom.hom (A.leftRegularHomEquiv.toModuleIso.hom ≫ (moduleCatCochainComplex A g).d i (i + 1))) x =
    (ModuleCat.Hom.hom
        (((resolution k g hg).complex.linearYonedaObj k A).d i (i + 1) ≫ A.leftRegularHomEquiv.toModuleIso.hom))
      x

Tactic:
simp [hi, Nat.even_add_one.2 hi, Representation.norm, homEquiv, Rep.norm, ← hom_comm_apply x]

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
x : ↑A
hx : (ConcreteCategory.hom (d₀₁ A)) x = 0
g : G
⊢ (A.ρ g) x - x = 0

Tactic:
exact congr_fun hx g

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

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
A : Rep k G
g : G
inst✝ : DecidableEq G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
hi : Odd i
x : ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker
⊢ (ConcreteCategory.hom (groupHomologyπOdd A g hg i hi)) x = 0 ↔ ↑x ∈ LinearMap.range A.ρ.norm

Tactic:
simp [groupHomologyπOdd, map_eq_zero_iff _ ((ModuleCat.mono_iff_injective _).1 inferInstance),
    ShortComplex.moduleCatToCycles, -LinearMap.mem_range, Rep.norm, LinearMap.range_codRestrict]

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Fintype G
X : FDRep k G
v : ↑X.V
t : G
f : ↑rightFDRep.V.obj
φ_term : (X : FDRep k G) → (G → k) → ↑X.V → G → ↑X.V := fun X f v s ↦ f s • (X.ρ s⁻¹) v
⊢ (Hom.hom (rightFDRep.ρ t ≫ InducedCategory.homMk (↟(sumSMulInv v))).hom) f =
    (Hom.hom (InducedCategory.homMk (↟(sumSMulInv v)) ≫ X.ρ t).hom) f

Tactic:
have := sum_map univ (mulRightEmbedding t⁻¹) (φ_term X (rightRegular t f) v)

Goal state after:
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : Fintype G
X : FDRep k G
v : ↑X.V
t : G
f : ↑rightFDRep.V.obj
φ_term : (X : FDRep k G) → (G → k) → ↑X.V → G → ↑X.V := fun X f v s ↦ f s • (X.ρ s⁻¹) v
this :
  ∑ x ∈ map (mulRightEmbedding t⁻¹) univ, φ_term X ((rightRegular t) f) v x =
    ∑ x, φ_term X ((rightRegular t) f) v ((mulRightEmbedding t⁻¹) x)
⊢ (Hom.hom (rightFDRep.ρ t ≫ InducedCategory.homMk (↟(sumSMulInv v))).hom) f =
    (Hom.hom (InducedCategory.homMk (↟(sumSMulInv v)) ≫ X.ρ t).hom) f
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: case h₁
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (Set.range fun gv ↦ (A.ρ gv.1) gv.2 - gv.2) ⊆ ↑(ModuleCat.Hom.hom (d₁₀ A)).range

Tactic:
rintro _ ⟨x, rfl⟩
    use single x.1⁻¹ x.2
    simp [d₁₀]

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

Goal state before:
pp: case h₂
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A
y : ↑(ModuleCat.of k (G →₀ ↑A))
hy : (ModuleCat.Hom.hom (d₁₀ A)) y = x
⊢ x ∈ Submodule.span k (Set.range fun gv ↦ (A.ρ gv.1) gv.2 - gv.2)

Tactic:
induction y using Finsupp.induction generalizing x with

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 : ↥(cycles₁ A)
⊢ (ConcreteCategory.hom (H1π A)) x = 0 ↔ ↑x ∈ boundaries₁ A

Tactic:
have h := leftHomologyπ_naturality'_assoc (isoShortComplexH1 A).inv
    (shortComplexH1 A).moduleCatLeftHomologyData (leftHomologyData _)
    ((inhomogeneousChains A).sc 1).leftHomologyIso.hom
  simp only [H1π, isoCycles₁, π, HomologicalComplex.homologyπ, homologyπ,
    cyclesMapIso'_inv, leftHomologyπ, ← h, ← leftHomologyMapIso'_inv, ModuleCat.hom_comp,
    LinearMap.coe_comp, Function.comp_apply, map_eq_zero_iff _
    ((ModuleCat.mono_iff_injective <| _).1 inferInstance)]
  simp [LinearMap.range_codRestrict, boundaries₁, shortComplexH1, cycles₁]

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

Goal state before:
pp: σ✝ : Type u_1
R✝ : Type u_2
n : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
x✝ : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
⊢ (↑↑(toAdicCompletion σ R).toRingHom).toFun (toAdicCompletionInv σ R x✝) = x✝

Tactic:
by ext; simpa using! mk_truncTotal_toAdicCompletionInv

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Pi

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : CommSemiring T
inst✝¹ : Algebra R S
inst✝ : Algebra S T
z : S
⊢ (algebraMap S T) ((aeval z) 1) = 1 z

Tactic:
simp only [Pi.one_apply, map_one]

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
ass : Ideal.comap (algebraMap R R') p ∈ associatedPrimes R M
⊢ p ∈ associatedPrimes R' M'

Tactic:
rcases ass with ⟨hp, x, hx⟩

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
⊢ p ∈ associatedPrimes R' M'
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
ass : p ∈ associatedPrimes R' M'
fg : (Ideal.comap (algebraMap R R') p).FG
⊢ Ideal.comap (algebraMap R R') p ∈ associatedPrimes R M

Tactic:
rcases ass with ⟨hp, x, hx⟩

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
fg : (Ideal.comap (algebraMap R R') p).FG
hp : p.IsPrime
x : M'
hx : p = (⊥.colon {x}).radical
⊢ Ideal.comap (algebraMap R R') p ∈ associatedPrimes R M
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n✝ : ℕ
x✝ : B
hx : x✝ ∉ J
⊢ e.symm x✝ ∉ I

Tactic:
rwa [symm_apply_mem_of_equiv_iff, h]

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
x✝ : B
hx : x✝ ∈ J
⊢ hI.dpow 0 (e.symm x✝) = 1

Tactic:
hI.dpow_zero

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
x✝ : B
hx : x✝ ∈ J
⊢ 1 = 1

A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
x✝ : B
hx : x✝ ∈ J
⊢ e.symm x✝ ∈ I
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
x✝ : B
hx : x✝ ∈ J
⊢ e.symm x✝ ∈ I

Tactic:
rwa [symm_apply_mem_of_equiv_iff, h]

Goal state after: