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

Goal state before:
pp: Ω : Type u_1
S : Type u_2
T : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
F : T → Type u_5
inst✝¹⁰ : (s : S) → TopologicalSpace (E s)
inst✝⁹ : (s : S) → MeasurableSpace (E s)
inst✝⁸ : ∀ (s : S), BorelSpace (E s)
inst✝⁷ : ∀ (s : S), HasOuterApproxClosed (E s)
inst✝⁶ : (t : T) → TopologicalSpace (F t)
inst✝⁵ : (t : T) → MeasurableSpace (F t)
inst✝⁴ : ∀ (t : T), BorelSpace (F t)
inst✝³ : ∀ (t : T), HasOuterApproxClosed (F t)
X : (s : S) → Ω → E s
Y : (t : T) → Ω → F t
inst✝² : Fintype S
inst✝¹ : Fintype T
inst✝ : IsFiniteMeasure P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h :
  ∀ (f : (s : S) → E s →ᵇ ℝ) (g : (t : T) → F t →ᵇ ℝ),
    ∫ (x : Ω), ((∏ s, ⇑(f s) ∘ X s) * ∏ t, ⇑(g t) ∘ Y t) x ∂P =
      (∫ (x : Ω), (∏ s, ⇑(f s) ∘ X s) x ∂P) * ∫ (x : Ω), (∏ t, ⇑(g t) ∘ Y t) x ∂P
⊢ (fun ω s ↦ X s ω) ⟂ᵢ[P] fun ω t ↦ Y t ω

Tactic:
by
  rw [indepFun_iff_map_prod_eq_prod_map_map (aemeasurable_pi_lambda _ mX)
    (aemeasurable_pi_lambda _ mY)]
  refine eq_prod_of_integral_prod_mul_prod_boundedContinuousFunction fun f g ↦ ?_
  rw [integral_map, integral_map, integral_map]
  · convert! h f g <;> simp
  any_goals fun_prop
  all_goals exact Measurable.aestronglyMeasurable (by fun_prop)

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

Goal state before:
pp: X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
h𝓑𝓧 : 𝓑 ≤ 𝓧
A : Set X
hA : MeasurableSet A
B : Set X
hB : MeasurableSet B
x : X
⊢ ((π.restrict ⋯) x) A = B.indicator 1 x * (π x) A ↔ (π x) (A ∩ B) = B.indicator 1 x * (π x) A

Tactic:
rw [restrict_apply, Measure.restrict_apply hA]

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

Goal state before:
pp: X : Type u_1
𝓑 𝓧 : MeasurableSpace X
π : Kernel X X
A B : Set X
hπ : π.IsProper
h𝓑𝓧 : 𝓑 ≤ 𝓧
μ : Measure X
hA : MeasurableSet A
hB : MeasurableSet B
⊢ ∫⁻ (a : X) in B, (π a) A ∂μ = (⇑π ∘ₘ μ) (A ∩ B)

Tactic:
rw [Measure.bind_apply (by measurability) (π.measurable.mono h𝓑𝓧 le_rfl).aemeasurable]
  simp only [hπ.inter_eq_indicator_mul h𝓑𝓧 hA hB, ← indicator_mul_const, Pi.one_apply, one_mul]
  rw [← lintegral_indicator (h𝓑𝓧 _ hB)]
  rfl

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

Goal state before:
pp: case refine_2
Ω : 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']
s t : Set Ω
h : μ[(s ∩ t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']
hs : s ∈ s1
ht : t ∈ s2
⊢ (fun ω ↦ ((condExpKernel μ m') ω) (s ∩ t)) =ᵐ[μ] fun i ↦ ((condExpKernel μ m') i) s * ((condExpKernel μ m') i) t

Tactic:
filter_upwards [hs1_eq s hs, hs2_eq t ht, hs12_eq s hs t ht, h] with ω hs_eq ht_eq hst_eq h

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']
s t : Set Ω
h✝ : μ[(s ∩ t).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']
hs : s ∈ s1
ht : t ∈ s2
ω : Ω
hs_eq : (((condExpKernel μ m') ω) s).toReal = μ[s.indicator fun ω ↦ 1 | m'] ω
ht_eq : (((condExpKernel μ m') ω) t).toReal = μ[t.indicator fun ω ↦ 1 | m'] ω
hst_eq : (((condExpKernel μ m') ω) (s ∩ t)).toReal = μ[(s ∩ t).indicator fun ω ↦ 1 | m'] ω
h : μ[(s ∩ t).indicator fun ω ↦ 1 | m'] ω = (μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']) ω
⊢ ((condExpKernel μ m') ω) (s ∩ t) = ((condExpKernel μ m') ω) s * ((condExpKernel μ m') ω) t
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
a✝ : (X₁✝.carrier × X₂✝.carrier) × X₃✝.carrier
s✝ : Set (Y₁✝.carrier × Y₂✝.carrier × Y₃✝.carrier)
hs : MeasurableSet s✝
⊢ (((κ₁.hom a✝.1.1).prod (κ₂.hom a✝.1.2)).prod (η.hom a✝.2)) (⇑prodAssoc ⁻¹' s✝) =
    ((κ₁.hom (prodAssoc a✝).1).prod ((κ₂.hom (prodAssoc a✝).2.1).prod (η.hom (prodAssoc a✝).2.2))) s✝

Tactic:
Measure.prod_apply hs,

Goal state after:
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
a✝ : (X₁✝.carrier × X₂✝.carrier) × X₃✝.carrier
s✝ : Set (Y₁✝.carrier × Y₂✝.carrier × Y₃✝.carrier)
hs : MeasurableSet s✝
⊢ (((κ₁.hom a✝.1.1).prod (κ₂.hom a✝.1.2)).prod (η.hom a✝.2)) (⇑prodAssoc ⁻¹' s✝) =
    ∫⁻ (x : Y₁✝.carrier),
      ((κ₂.hom (prodAssoc a✝).2.1).prod (η.hom (prodAssoc a✝).2.2)) (Prod.mk x ⁻¹' s✝) ∂κ₁.hom (prodAssoc a✝).1
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst✝² : Nonempty Y
mY : MeasurableSpace Y
inst✝¹ : StandardBorelSpace Y
κ : Kernel X Y
inst✝ : IsMarkovKernel κ
g : Y → ↑I := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (κ.map g)
hg'κ : κ = (κ.map g).map hg.invFun
f' : X → ↑I → ↑I
hf' : Measurable (uncurry f')
hf'κ : ∀ (a : X), Measure.map (f' a) volume = (κ.map g) a
a : X
⊢ Measure.map ((fun a u ↦ hg.invFun (f' a u)) a) volume = Measure.map hg.invFun ((κ.map g) a)

Tactic:
← hf'κ,

Goal state after:
X : Type u_1
Y : Type u_2
mX : MeasurableSpace X
inst✝² : Nonempty Y
mY : MeasurableSpace Y
inst✝¹ : StandardBorelSpace Y
κ : Kernel X Y
inst✝ : IsMarkovKernel κ
g : Y → ↑I := sigmoid ∘ embeddingReal Y
hg : MeasurableEmbedding (sigmoid ∘ embeddingReal Y)
hκg : IsMarkovKernel (κ.map g)
hg'κ : κ = (κ.map g).map hg.invFun
f' : X → ↑I → ↑I
hf' : Measurable (uncurry f')
hf'κ : ∀ (a : X), Measure.map (f' a) volume = (κ.map g) a
a : X
⊢ Measure.map ((fun a u ↦ hg.invFun (f' a u)) a) volume = Measure.map hg.invFun (Measure.map (f' a) volume)
Module: Mathlib.Probability.ProbabilityMassFunction.Integrals

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSingletonClass α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : PMF α
f : α → E
hf : Integrable f p.toMeasure
⊢ ∫ (a : α), f a ∂p.toMeasure = ∫ (a : α) in p.support, f a ∂p.toMeasure

Tactic:
rw [restrict_toMeasure_support p]

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Integrals

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSingletonClass α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : PMF α
f : α → E
hf : Integrable f p.toMeasure
⊢ ∫ (a : α) in p.support, f a ∂p.toMeasure = ∑' (a : ↑p.support), (p.toMeasure {↑a}).toReal • f ↑a

Tactic:
apply setIntegral_countable f p.support_countable
    rwa [IntegrableOn, restrict_toMeasure_support p]

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_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑κ ∘ₘ ν)
h_mgf : ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℚ), mgf X (κ a) ↑i ≤ rexp (↑c * ↑i ^ 2 / 2)
h_int' : ∀ (n : ℤ), ∀ᵐ (x : Ω') ∂ν, Integrable (fun ω ↦ rexp (↑n * X ω)) (κ x)
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')

Tactic:
rw [← ae_all_iff] at h_int'

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑κ ∘ₘ ν)
h_mgf : ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℚ), mgf X (κ a) ↑i ≤ rexp (↑c * ↑i ^ 2 / 2)
h_int' : ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℤ), Integrable (fun ω ↦ rexp (↑i * X ω)) (κ a)
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
N : Submodule A[G] ρ.asModule
g : G
w : W
hw : w ∈ { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }
x✝ : Module A[G] W := ρ.instModuleMonoidAlgebraAsModule
⊢ (ρ g) w ∈ { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }

Tactic:
have h : (MonoidAlgebra.single g (1 : A)) • w ∈ N :=
      Submodule.smul_of_tower_mem N _ hw

Goal state after:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
N : Submodule A[G] ρ.asModule
g : G
w : W
hw : w ∈ { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }
x✝ : Module A[G] W := ρ.instModuleMonoidAlgebraAsModule
h : MonoidAlgebra.single g 1 • w ∈ N
⊢ (ρ g) w ∈ { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e_f.e_a.hs
Ω : 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 : ℕ
⊢ ∀ i_1 ∈ range (u i), MemLp (Y i_1) 2 ℙ

Tactic:
intro j _

Goal state after:
case e_f.e_a.hs
Ω : 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 j : ℕ
a✝ : j ∈ range (u i)
⊢ MemLp (Y j) 2 ℙ
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)
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
N : ℕ
⊢ ENNReal.ofReal (∑ i ∈ range N, Var[S (u i); ℙ] / (↑(u i) * ε) ^ 2) ≤ ENNReal.ofReal (ε⁻¹ ^ 2 * C)

Tactic:
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.FDRep

Goal state before:
pp: R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
X Y : FDRep R G
f : X ⟶ Y
g : G
x : ↑(((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj X).V
⊢ (ModuleCat.Hom.hom ((forget₂ (FGModuleCat R) (ModuleCat R)).map f.hom) ∘ₗ
        ((((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj X).V.endRingEquiv.toMonoidHom.comp
            (((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj X).ρ)
          g)
      x =
    (((((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj Y).V.endRingEquiv.toMonoidHom.comp
            (((forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).obj Y).ρ)
          g ∘ₗ
        ModuleCat.Hom.hom ((forget₂ (FGModuleCat R) (ModuleCat R)).map f.hom))
      x

Tactic:
exact ConcreteCategory.congr_hom ((forget (FGModuleCat R)).congr_map (f.comm g)) x

Goal state after:
Module: Mathlib.RepresentationTheory.Irreducible

Goal state before:
pp: G : Type u_1
k : Type u_2
V : Type u_3
inst✝³ : Monoid G
inst✝² : Field k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
⊢ ρ.IsIrreducible ↔ IsSimpleModule k[G] ρ.asModule

Tactic:
by
  rw [isSimpleModule_iff]
  exact OrderIso.isSimpleOrder_iff Subrepresentation.subrepresentationSubmoduleOrderIso

Goal state after:
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: 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)
⊢ (↑(Nat.card G))⁻¹ * ∑ x, (ρ.linHom σ).character x = ↑(finrank k (ρ.IntertwiningMap σ))

Tactic:
card_inv_mul_sum_char_eq_finrank,

Goal state after:
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)
⊢ ↑(finrank k ↥(ρ.linHom σ).invariants) = ↑(finrank k (ρ.IntertwiningMap σ))
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : Monoid H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
σ : Representation k G A
ρ : Representation k G B
f : σ.IntertwiningMap ρ
x : H → A
h : x ∈ coindV φ σ
⊢ (f.compLeft H) x ∈ coindV φ ρ

Tactic:
simp only [mem_coindV, LinearMap.compLeft_apply, Function.comp_apply,
      IntertwiningMap.toLinearMap_apply] at h ⊢
    intro g h0
    simpa [h] using LinearMap.ext_iff.1 (f.2 g) (x h0)

Goal state after:
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: case refine_2
k : Type u
G✝ : Type v
H : Type w
inst✝⁴ : CommRing k
inst✝³ : Monoid G✝
inst✝² : Monoid H
φ : G✝ →* H
A : Rep k G✝
G : Type v'
inst✝¹ : Group G
S : Subgroup G
X Y : Rep k ↥S
f : X ⟶ Y
inst✝ : Epi f
y : ↑((coindFunctor k S.subtype).obj Y)
this : Setoid G := QuotientGroup.rightRel S
s : ↑Y → ↑X
hs : ∀ (b : ↑Y), (Hom.hom f) (s b) = b
i : Quotient this → G
hi : ∀ (b : Quotient this), Quotient.mk' (i b) = b
γ : G → ↥S := fun g ↦ ⟨g * (i (Quotient.mk' g))⁻¹, ⋯⟩
hmk : ∀ (s : ↥S) (g : G), Quotient.mk' (↑s * g) = Quotient.mk' g
hγ : ∀ (s : ↥S) (g : G), γ (↑s * g) = s * γ g
x : G → ↑X := fun g ↦ (X.ρ (γ g)) (s (↑y (i (Quotient.mk' g))))
g : G
⊢ (Y.ρ (γ g)) ((Hom.hom f) (s (↑y (i (Quotient.mk' g))))) = ↑y g

Tactic:
simp_all [← y.2 (γ g), γ]

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

Goal state before:
pp: case refine_1.succ
k : Type u_1
G : Type u_2
inst✝⁴ : CommRing k
inst✝³ : Group G
V : Type u_4
inst✝² : AddCommGroup V
inst✝¹ : Module k V
ρ : Representation k G V
g : G
inst✝ : Finite G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
α : V
n : ℕ
a✝ : (fun gv ↦ (ρ gv.1) gv.2 - gv.2) ((fun x ↦ g ^ x) n, α) ∈ ↑(ρ g - LinearMap.id).range
⊢ (fun gv ↦ (ρ gv.1) gv.2 - gv.2) ((fun x ↦ g ^ x) (n + 1), α) ∈ ↑(ρ g - LinearMap.id).range

Tactic:
use (Fin.partialSum (fun (j : Fin (n + 1)) => ρ (g ^ (j : ℕ)) α) (Fin.last _))

Goal state after:
case h
k : Type u_1
G : Type u_2
inst✝⁴ : CommRing k
inst✝³ : Group G
V : Type u_4
inst✝² : AddCommGroup V
inst✝¹ : Module k V
ρ : Representation k G V
g : G
inst✝ : Finite G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
α : V
n : ℕ
a✝ : (fun gv ↦ (ρ gv.1) gv.2 - gv.2) ((fun x ↦ g ^ x) n, α) ∈ ↑(ρ g - LinearMap.id).range
⊢ (ρ g - LinearMap.id) (Fin.partialSum (fun j ↦ (ρ (g ^ ↑j)) α) (Fin.last (n + 1))) =
    (fun gv ↦ (ρ gv.1) gv.2 - gv.2) ((fun x ↦ g ^ x) (n + 1), α)
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f₁ f₂ : G →* H
h : f₁ = f₂
φ : res f₁ A ⟶ B
T : Type u_1
F : (f : G →* H) → (res f A ⟶ B) → T
⊢ F f₁ φ = F f₂ (h ▸ φ)

Tactic:
subst h
  rfl

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
γ : Type u_3
R : Type u_4
f : σ → τ
g : τ → γ
inst✝² : TendstoCofinite f
inst✝¹ : CommSemiring R
inst✝ : TendstoCofinite g
p : MvPowerSeries σ R
y : γ →₀ ℕ
⊢ ∑ p_1 ∈ Finset.image (fun u ↦ (mapDomain f u, u)) ⋯.toFinset, (coeff p_1.2) p = ∑ x ∈ ⋯.toFinset, (coeff x) p

Tactic:
Finset.sum_image (by simp)

Goal state after:
σ : Type u_1
τ : Type u_2
γ : Type u_3
R : Type u_4
f : σ → τ
g : τ → γ
inst✝² : TendstoCofinite f
inst✝¹ : CommSemiring R
inst✝ : TendstoCofinite g
p : MvPowerSeries σ R
y : γ →₀ ℕ
⊢ ∑ x ∈ ⋯.toFinset, (coeff (mapDomain f x, x).2) p = ∑ x ∈ ⋯.toFinset, (coeff x) p
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
g : G
a : ↑A
⊢ single g a ∈ cycles₁ A ↔ (A.ρ g) a = a

Tactic:
simp [mem_cycles₁_iff, ← (A.ρ.apply_bijective g).1.eq_iff (a := A.ρ g⁻¹ a), eq_comm]

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
g : G
a : ↑A
⊢ single g⁻¹ ((A.ρ g⁻¹) a) + single g a ∈ boundaries₁ A

Tactic:
← d₂₁_single_inv_mul_ρ_add_single g 1

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
g : G
a : ↑A
⊢ (ConcreteCategory.hom (d₂₁ A)) (single (g⁻¹, g * 1) ((A.ρ g⁻¹) a) + single (g, 1) a) ∈ boundaries₁ A
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hXI : X ∈ I
⊢ Ideal.map (C.comp constantCoeff) I ≤ I

Tactic:
by
  suffices ∀ x ∈ I, C (constantCoeff x) ∈ I by simpa [Ideal.map_le_iff_le_comap]
  intro f hf
  rw [← sub_eq_iff_eq_add'.mpr f.eq_X_mul_shift_add_const]
  exact sub_mem hf (I.mul_mem_right _ hXI)

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hXI : X ∉ I
n✝ : ℕ
F : Fin n✝ → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' : Ideal.map constantCoeff I = span (Set.range (⇑constantCoeff ∘ F))
T : R⟦X⟧ → Fin n✝ → R
hT : ∀ g ∈ I, ∑ i, T g i * constantCoeff (F i) = constantCoeff g
g : R⟦X⟧
hg : g ∈ I
G : ℕ → R⟦X⟧ := fun t ↦ Nat.rec g (fun x G' ↦ mk fun p ↦ (coeff (p + 1)) G' - ∑ i, T G' i * (coeff (p + 1)) (F i)) t
hG : ∀ (n : ℕ), G n ∈ I
hG' : ∀ (n : ℕ), G n - ∑ i, C (T (G n) i) * F i = X * G (n + 1)
H : Fin n✝ → R⟦X⟧ := fun i ↦ mk fun n ↦ T (G n) i
h₁ : ∀ (n : ℕ), g - ∑ i, ↑((trunc n) (H i)) * F i = X ^ n * G n
n : ℕ
⊢ (coeff n) g = (coeff n) (∑ i, H i * F i)

Tactic:
simpa [coeff_trunc, sub_eq_zero] using congr(($(h₁ (n + 1)).trunc (n + 1)).coeff n)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (i j : ℕ), ∃ k, I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j

Tactic:
intro i j

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
i j : ℕ
⊢ ∃ k, I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
⊢ P.FG → (Ideal.map constantCoeff P).FG

pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
⊢ (Ideal.map constantCoeff P).FG → P.FG

Tactic:
· exact (FG.map · _)

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
⊢ (Ideal.map constantCoeff P).FG → P.FG
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H : top = J.adicTopology
⊢ (∀ (n : ℕ), IsOpen[top] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s

Tactic:
rw [H]

Goal state after:
case mp
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
H : top = J.adicTopology
⊢ (∀ (n : ℕ), IsOpen[J.adicTopology] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f₁ f₂ : G →* H
h : f₁ = f₂
φ : A ⟶ res f₁ B
T : Type u_1
F : (f : G →* H) → (A ⟶ res f B) → T
⊢ F f₁ φ = F f₂ (h ▸ φ)

Tactic:
subst h
  rfl

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
x : σ →₀ ℕ
p : MvPowerSeries σ R
n : ℕ
hx : degree x < n
⊢ MvPolynomial.coeff x (Quotient.out (↑((toAdicCompletion σ R) p) n) - (truncTotal n) p) = 0

Tactic:
apply (MvPolynomial.mem_pow_idealOfVars_iff' n _).mp

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
x : σ →₀ ℕ
p : MvPowerSeries σ R
n : ℕ
hx : degree x < n
⊢ Quotient.out (↑((toAdicCompletion σ R) p) n) - (truncTotal n) p ∈ MvPolynomial.idealOfVars σ R ^ n

case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
x : σ →₀ ℕ
p : MvPowerSeries σ R
n : ℕ
hx : degree x < n
⊢ degree x < n
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
x : σ →₀ ℕ
p : MvPowerSeries σ R
n : ℕ
hx : degree x < n
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n * ⊤))
      (Quotient.out ((Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n * ⊤)) ((truncTotal n) p))) =
    (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n * ⊤)) ((truncTotal n) p)

Tactic:
Ideal.Quotient.mk_out

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
x : σ →₀ ℕ
p : MvPowerSeries σ R
n : ℕ
hx : degree x < n
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n * ⊤)) ((truncTotal n) p) =
    (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n * ⊤)) ((truncTotal n) p)
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h : ¬p.coeff n = 0
⊢ p.coeff n ∈ p.contentIdeal

Tactic:
apply subset_span

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
h : ¬p.coeff n = 0
⊢ p.coeff n ∈ ↑p.coeffs
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: case mpr
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
⊢ C r ∣ p → p.contentIdeal ≤ span {r}

Tactic:
rw [← contentIdeal_C r]

Goal state after:
case mpr
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
r : R
⊢ C r ∣ p → p.contentIdeal ≤ (C r).contentIdeal