mathlib-initiative/mathlib-tactics huggingface dataset:
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
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
⊢ Measure.map (fun ω ↦ (k ω, g ω, f ω)) μ =
      ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ ↔
    Measure.map (fun x ↦ ((k x, g x), f x)) μ =
      ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun ω ↦ (k ω, g ω)) μ

Tactic:
← h_eq

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
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
⊢ Measure.map (fun ω ↦ (k ω, g ω, f ω)) μ =
      ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ ↔
    Measure.map (fun x ↦ ((k x, g x), f x)) μ =
      ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ
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
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
⊢ Measure.map (fun ω ↦ (k ω, g ω, f ω)) μ =
      ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ ↔
    Measure.map (fun x ↦ ((k x, g x), f x)) μ =
      ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ

Tactic:
have h1 : μ.map (fun x ↦ ((k x, g x), f x)) = (μ.map (fun a ↦ (k a, g a, f a))).map e := by
    rw [Measure.map_map (by fun_prop) (by fun_prop)]
    rfl

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
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
h1 : Measure.map (fun x ↦ ((k x, g x), f x)) μ = Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ)
⊢ Measure.map (fun ω ↦ (k ω, g ω, f ω)) μ =
      ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ ↔
    Measure.map (fun x ↦ ((k x, g x), f x)) μ =
      ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
g : Ω → E
s : Set Ω
⊢ (∫ (x : Ω) in s, g x ∂μ.tilted fun x ↦ t * X x) = ∫ (x : Ω) in s, (rexp (t * X x) / mgf X μ t) • g x ∂μ

Tactic:
by
  rw [setIntegral_tilted, mgf]

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
Y : Ω → ℝ
h : HasSubgaussianMGF X c κ ν
h' : X =ᵐ[⇑κ ∘ₘ ν] Y
h'' : ∀ᵐ (ω' : Ω') ∂ν, ∀ᵐ (ω : Ω) ∂κ ω', X ω = Y ω
ω' : Ω'
h_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
⊢ (∀ᵐ (ω : Ω) ∂κ ω', X ω = Y ω) → ∀ (t : ℝ), mgf Y (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
h'

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Y : Ω → ℝ
h : HasSubgaussianMGF X c κ ν
h'✝ : X =ᵐ[⇑κ ∘ₘ ν] Y
h'' : ∀ᵐ (ω' : Ω') ∂ν, ∀ᵐ (ω : Ω) ∂κ ω', X ω = Y ω
ω' : Ω'
h_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
h' : ∀ᵐ (ω : Ω) ∂κ ω', X ω = Y ω
⊢ ∀ (t : ℝ), mgf Y (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
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
inst✝ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
⊢ ∃ nk, StrictMono nk ∧ IsPreLocalizingSequence 𝓕 (fun i ω ↦ min (τ i ω) (σ i (nk i) ω)) P

Tactic:
obtain ⟨nk, T, hnk, hT, hP⟩ := isPreLocalizingSequence_of_isLocalizingSequence_aux hτ hσ

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : ConditionallyCompleteLinearOrderBot ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝² : SecondCountableTopology ι
inst✝¹ : IsFiniteMeasure P
inst✝ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
nk : ℕ → ℕ
T : ℕ → ι
hnk : StrictMono nk
hT : Tendsto T atTop atTop
hP : ∀ (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n
⊢ ∃ nk, StrictMono nk ∧ IsPreLocalizingSequence 𝓕 (fun i ω ↦ min (τ i ω) (σ i (nk i) ω)) P
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A : ∑ j ∈ range K, ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ ≤ (∫ (a : Ω), X a) + 1
a b : ℝ
⊢ ℙ {ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)

Tactic:
rw [ofReal_setIntegral_one ρ _,
      Measure.map_apply_of_aemeasurable hint.aemeasurable measurableSet_Ioc]

Goal state after:
Ω : 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 ρ
A : ∑ j ∈ range K, ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ ≤ (∫ (a : Ω), X a) + 1
a b : ℝ
⊢ ℙ {ω | X ω ∈ Set.Ioc a b} = ℙ (X ⁻¹' Set.Ioc a b)
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 : ℝ
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 N, (↑(u i) ^ 2)⁻¹ * ∑ j ∈ range (u i), Var[Y j; ℙ] =
    ∑ j ∈ range (u (N - 1)), (∑ i ∈ range N with j < u i, (↑(u i) ^ 2)⁻¹) * Var[Y j; ℙ]

Tactic:
simp_rw [mul_sum, sum_mul, sum_sigma']
        refine sum_nbij' (fun p ↦ ⟨p.2, p.1⟩) (fun p ↦ ⟨p.2, p.1⟩) ?_ ?_ ?_ ?_ ?_
        · simp only [mem_sigma, mem_range, mem_filter, and_imp,
            Sigma.forall]
          exact fun a b haN hb ↦ ⟨hb.trans_le <| u_mono <| Nat.le_pred_of_lt haN, haN, hb⟩
        all_goals simp

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: case add
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 : ρ.IntertwiningMap σ
v : ρ.asModule
x y : A[G]
hx : f.toLinearMap (x • v) = (RingHom.id A[G]) x • f.toLinearMap v
hy : f.toLinearMap (y • v) = (RingHom.id A[G]) y • f.toLinearMap v
⊢ f.toLinearMap ((x + y) • v) = (RingHom.id A[G]) (x + y) • f.toLinearMap v

Tactic:
simp [add_smul, map_add, hx, hy]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:

Tactic:
∑ i ∈ range N, ℙ {ω | (u i * ε : ℝ) ≤ |S (u i) ω - 𝔼[S (u i)]|} ≤
          ∑ i ∈ range N, ENNReal.ofReal (Var[S (u i)] / (u i * ε) ^ 2) := by
        gcongr with i _
        apply meas_ge_le_variance_div_sq
        · exact memLp_finsetSum' _ fun j _ => (hident j).aestronglyMeasurable_fst.memLp_truncation
        · apply mul_pos (Nat.cast_pos.2 _) εpos
          refine zero_lt_one.trans_le ?_
          apply Nat.le_floor
          rw [Nat.cast_one]
          apply one_le_pow₀ c_one.le
      _ = ENNReal.ofReal (∑ i ∈ range N, Var[S (u i)] / (u i * ε) ^ 2) := by
        rw [ENNReal.ofReal_sum_of_nonneg fun i _ => ?_]
        exact div_nonneg (variance_nonneg _ _) (sq_nonneg _)
      _ ≤ ENNReal.ofReal (ε⁻¹ ^ 2 * C) := by
        apply ENNReal.ofReal_le_ofReal
        simp_rw [div_eq_inv_mul, ← inv_pow, mul_inv, mul_comm _ (ε⁻¹), mul_pow, mul_assoc,
          ← mul_sum]
        gcongr
        simpa only [inv_pow] using I2 N

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

pp: case mpr
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.ShortExact → (S.map (resFunctor φ)).ShortExact

Tactic:
· intro h
    have h₁ := h.1
    have h₂ := h.2
    have h₃ := h.3
    rw [ShortComplex.exact_map_iff_of_faithful] at h₁
    simp only [ShortComplex.map_f, mono_iff_injective, ShortComplex.map_g,
      epi_iff_surjective] at h₂ h₃
    exact {exact := h₁, mono_f := mono_iff_injective _|>.2 h₂, epi_g := epi_iff_surjective _|>.2 h₃}

Goal state after:
case mpr
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.ShortExact → (S.map (resFunctor φ)).ShortExact
Module: Mathlib.RepresentationTheory.Rep.Iso

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
⊢ ↑V ≃+ ↑((toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra).obj V)

Tactic:
by
  dsimp [ofModuleMonoidAlgebra, toModuleMonoidAlgebra]
  exact V.ρ.asModuleEquiv.symm.toAddEquiv.trans (RestrictScalars.addEquiv _ _ _).symm

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) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
⊢ ∑' (j : ℕ), ℙ {ω | X j ω ∈ Set.Ioi ↑j} < ∞

Tactic:
convert! tsum_prob_mem_Ioi_lt_top hint (hnonneg 0) using 2

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
⊢ (fun j ↦ ℙ {ω | X j ω ∈ Set.Ioi ↑j}) = fun j ↦ ℙ {ω | X 0 ω ∈ Set.Ioi ↑j}
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: 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
r : k
v : V
hv : v ∈ {v | ∀ (g : G), (ρ g) v = v}
g : G
⊢ (ρ g) (r • v) = r • v

Tactic:
by simp only [hv g, map_smulₛₗ, RingHom.id_apply]

Goal state after:
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
    rw [← LinearMap.comp_assoc, ← h, LinearMap.comp_assoc, ← Rep.ρ_mul, mul_inv_cancel, map_one,
      Module.End.one_eq_id, LinearMap.comp_id]

Goal state after:
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: case inr
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst✝¹² : Group G
inst✝¹¹ : Field k
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module k V
inst✝⁸ : FiniteDimensional k V
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k W
inst✝⁵ : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
inst✝⁴ : Fintype G
inst✝³ : Invertible ↑(Nat.card G)
inst✝² : IsAlgClosed k
inst✝¹ : ρ.IsIrreducible
inst✝ : σ.IsIrreducible
h✝ : Nonempty (σ.Equiv ρ)
φ : σ.Equiv ρ
⊢ (↑(Nat.card G))⁻¹ * ∑ g, ρ.character g * σ.character g⁻¹ = if Nonempty (σ.Equiv ρ) then 1 else 0

Tactic:
char_iso φ,

Goal state after:
case inr
G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst✝¹² : Group G
inst✝¹¹ : Field k
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module k V
inst✝⁸ : FiniteDimensional k V
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module k W
inst✝⁵ : FiniteDimensional k W
ρ : Representation k G V
σ : Representation k G W
inst✝⁴ : Fintype G
inst✝³ : Invertible ↑(Nat.card G)
inst✝² : IsAlgClosed k
inst✝¹ : ρ.IsIrreducible
inst✝ : σ.IsIrreducible
h✝ : Nonempty (σ.Equiv ρ)
φ : σ.Equiv ρ
⊢ (↑(Nat.card G))⁻¹ * ∑ g, ρ.character g * ρ.character g⁻¹ = if Nonempty (σ.Equiv ρ) then 1 else 0
Module: Mathlib.RepresentationTheory.Character

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

Tactic:
ext g; convert! trace_tensorProduct' (V.ρ g) (W.ρ g)

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e'_5
Ω : 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
hφ : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))
hψ : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, ψ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ))
ω : Ω
hωφ : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))
hωψ : Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, ψ (X i ω)) atTop (𝓝 (∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ))
⊢ 𝓝 (∫ (x : Ω), (⇑(φ + ψ) ∘ X 0) x ∂μ) = 𝓝 (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ + ∫ (x : Ω), (⇑ψ ∘ X 0) x ∂μ)

Tactic:
· congr 1
      rw [← integral_add]
      · rfl
      · exact (φ.comp (X 0) h').integrable_of_isFiniteMeasure
      · exact (ψ.comp (X 0) h').integrable_of_isFiniteMeasure

Goal state after:
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X : Rep k G
Y : ModuleCat k
f : X ⟶ (trivialFunctor k G).obj Y
⊢ ((coinvariantsAdjunction k G).homEquiv X Y).symm f = desc f

Tactic:
by
  ext
  simp [coinvariantsAdjunction, Adjunction.homEquiv_symm_apply]

Goal state after:
Module: Mathlib.RepresentationTheory.Continuous.TopRep

Goal state before:
pp: k : Type u
G : Type v
inst✝² : TopologicalSpace k
inst✝¹ : Ring k
inst✝ : Monoid G
A B C : TopRep k G
f g : A ⟶ B
h : B ⟶ C
⊢ Hom.hom ((f + g) ≫ h) = Hom.hom (f ≫ h + g ≫ h)

Tactic:
simp [hom_add, ContIntertwiningMap.comp_add]

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

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Ring k
inst✝ : Monoid G
A B C X : Rep k G
f : X ⟶ trivial k G PUnit.{w + 1}
⊢ f = default

Tactic:
by ext

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: k : Type u
G : Type v
inst✝³ : CommRing k
inst✝² : Group G
S : Subgroup G
inst✝¹ : DecidableRel ⇑(QuotientGroup.rightRel S)
inst✝ : S.FiniteIndex
A : Rep.{max w u v, u, v} k ↥S
B : Rep.{max w u v, u, v} k G
f : res S.subtype B ⟶ A
⊢ ((resIndAdjunction k S).homEquiv B A) f = (resCoindHomEquiv.{max w u v, u, v, v} S.subtype B A) f ≫ A.indCoindIso.inv

Tactic:
by
  rw [resIndAdjunction, Adjunction.homEquiv_ofNatIsoRight_apply]
  simp [resCoindHomEquiv]

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

Goal state before:
pp: 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 : ℕ
h₀ : NeZero i
hi : Even i
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap ≫ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝

Tactic:
simp [sub_hom]

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

Goal state before:
pp: 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 : ℕ
h₀ : NeZero i
hi : Even i
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝

Tactic:
simp [sub_hom]

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

Goal state before:
pp: 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 : ℕ
hi : Odd i
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap ≫ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝

Tactic:
simp [sub_hom]

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

Goal state before:
pp: 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 : ℕ
hi : Odd i
x✝ : ↑(ModuleCat.of k ↑A)
⊢ (ModuleCat.Hom.hom
        (ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap))
      x✝ =
    (ModuleCat.Hom.hom 0) x✝

Tactic:
simp [sub_hom]

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
hx : (Algebra.norm K) x = 1
xu : Lˣ := ⋯.unit
hx' : ↑(toMul (toAdditive ((Hom.hom (ofAlgebraAutOnUnits K L).norm) (toAdditive.symm (ofMul xu))))) = 1
⊢ ∃ y, g ↑y / ↑y = x

Tactic:
have := FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iff (ofAlgebraAutOnUnits K L) g hg
    1 (by simp) ⟨toAdditive.symm <| ofMul xu, by simp_all⟩

Goal state after:
K L : Type
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
inst✝ : IsCyclic Gal(L/K)
g : Gal(L/K)
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
x✝ : L
hx✝ : (Algebra.norm K) x✝ = 1
x : L
hx : (Algebra.norm K) x = 1
xu : Lˣ := ⋯.unit
hx' : ↑(toMul (toAdditive ((Hom.hom (ofAlgebraAutOnUnits K L).norm) (toAdditive.symm (ofMul xu))))) = 1
this :
  (CategoryTheory.ConcreteCategory.hom (FiniteCyclicGroup.groupCohomologyπOdd (ofAlgebraAutOnUnits K L) g hg 1 ⋯))
        ⟨toAdditive.symm (ofMul xu), ⋯⟩ =
      0 ↔
    ↑⟨toAdditive.symm (ofMul xu), ⋯⟩ ∈
      (Hom.hom
          ((ofAlgebraAutOnUnits K L).applyAsHom g - CategoryTheory.CategoryStruct.id (ofAlgebraAutOnUnits K L))).range
⊢ ∃ y, g ↑y / ↑y = x
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: A : Type u_3
σ : Type u_4
inst✝ : CommRing A
I : Ideal (MvPolynomial σ A)
d : MvPolynomial σ A
⊢ (aeval fun d ↦ (Ideal.Quotient.mk I) (X d)) d =
    eval₂ (algebraMap A (MvPolynomial σ A ⧸ I)) (fun d ↦ (Ideal.Quotient.mk I) (X d)) d

Tactic:
aeval,

Goal state after:
A : Type u_3
σ : Type u_4
inst✝ : CommRing A
I : Ideal (MvPolynomial σ A)
d : MvPolynomial σ A
⊢ { toRingHom := eval₂Hom (algebraMap A (MvPolynomial σ A ⧸ I)) fun d ↦ (Ideal.Quotient.mk I) (X d), commutes' := ⋯ }
      d =
    eval₂ (algebraMap A (MvPolynomial σ A ⧸ I)) (fun d ↦ (Ideal.Quotient.mk I) (X d)) d
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
⊢ span {a} ∉ kaplanskySet (closure {r | Prime r}).toSubsemigroup

Tactic:
by
  have hzero : 0 ∉ closure {r : R | Prime r} := fun h ↦ by
    rcases exists_multiset_of_mem_closure h with ⟨l, hl, hprod⟩
    exact not_prime_zero (hl 0 (Multiset.prod_eq_zero_iff.1 hprod))
  intro h
  rcases exists_mem_kaplanskySet_eq_of_le hzero with ⟨T, hT, hT₂⟩
  have hT₃ : T ≠ ⊥ := fun h₂ ↦ ha (span_singleton_eq_bot.1 ((h₂ ▸ hT₂) _ h zero_le))
  have Tpri := isPrime_of_maximally_disjoint T _ hT (fun J hJ H ↦ hJ.ne (hT₂ J H hJ.le).symm)
  rcases (H T) hT₃ Tpri with ⟨x, H₃, H₄⟩
  rw [mem_kaplanskySet_iff, eq_empty_iff_forall_notMem] at hT
  exact hT x ⟨H₃, subset_closure H₄⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ (∃ i, True ∧ ↑(I ^ i) ⊆ U) → ∃ i ∈ I.ringFilterBasis.toAddGroupFilterBasis, id i ⊆ U

Tactic:
rintro ⟨i, -, h⟩

Goal state after:
case mpr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : ↑(I ^ i) ⊆ U
⊢ ∃ i ∈ I.ringFilterBasis.toAddGroupFilterBasis, id i ⊆ U
Module: Mathlib.RingTheory.Bialgebra.GroupLike

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
a b : A
ha : IsGroupLikeElem R a
hb : IsGroupLikeElem R b
⊢ counit (a * b) = 1

Tactic:
simp [ha, hb]

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.GroupLike

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
a b : A
ha : IsGroupLikeElem R a
hb : IsGroupLikeElem R b
⊢ comul (a * b) = (a * b) ⊗ₜ[R] (a * b)

Tactic:
simp [ha, hb]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R), ∑ x ∈ s ×ˢ s, f x • x.1 ⊗ₜ[R] x.2 = ∑ x ∈ s ×ˢ s, g x • x.1 ⊗ₜ[R] x.2 → ∀ i ∈ s ×ˢ s, f i = g i
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
x : A
hx : x ∈ s
hcx : c x ≠ 0
y : A
hys : y ∈ s
hyx : y ≠ x
⊢ (y, x) ∈ s ×ˢ s

Tactic:
by simp [*]

Goal state after: