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

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

Tactic:
rw [tilted_apply_eq_ofReal_integral _ s, mgf]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst✝ : SFinite μ
s : Set Ω
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
⊢ (μ.tilted fun x ↦ t * X x) s = ENNReal.ofReal (∫ (a : Ω) in s, rexp (t * X a - cgf X μ t) ∂μ)

Tactic:
rcases eq_zero_or_neZero μ with rfl | hμ
  · simp
  · simp_rw [tilted_mul_apply_eq_ofReal_integral_mgf s, exp_sub]
    rwa [exp_cgf]

Goal state after:
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
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < P {ω | σ n k ω < min (τ n ω) ↑(T n)}
ω : Ω
i j : ℕ
hω : (fun x ↦ σ n x ω) i ≤ (fun x ↦ σ n x ω) j
hij : i ≤ j
⊢ (fun x ↦ σ n x ω < min (τ n ω) ↑(T n)) j ≤ (fun x ↦ σ n x ω < min (τ n ω) ↑(T n)) i

Tactic:
simp [Set.ofPred] at *

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
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
ω : Ω
i j : ℕ
hω : σ n i ω ≤ σ n j ω
hij : i ≤ j
hn : ∀ (k : ℕ), 2⁻¹ ^ n < P fun ω ↦ σ n k ω < τ n ω ∧ σ n k ω < ↑(T n)
⊢ σ n j ω < τ n ω → σ n j ω < ↑(T n) → σ n i ω < τ n ω ∧ σ n i ω < ↑(T n)
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : Semiring 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 σ
g : G
⊢ ∀ ⦃v : V⦄, v ∈ f.ker → (ρ g) v ∈ f.ker

Tactic:
simp +contextual [f.isIntertwining]

Goal state after:
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 _
          exact (hident j).aestronglyMeasurable_fst.memLp_truncation

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁹ : CommSemiring A
inst✝⁸ : Monoid G
inst✝⁷ : AddCommMonoid V
inst✝⁶ : AddCommMonoid W
inst✝⁵ : AddCommMonoid U
inst✝⁴ : Module A V
inst✝³ : Module A W
inst✝² : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module A P
π : Representation A G P
f : ρ.IntertwiningMap σ
g₁ g₂ : τ.IntertwiningMap π
⊢ f.tensor (g₁ + g₂) = f.tensor g₁ + f.tensor g₂

Tactic:
by ext; simp [TensorProduct.tmul_add]

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

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

Tactic:
dsimp

Goal state after:
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
X Y : Rep k G
f : ↑X →ₗ[k] ↑Y
g : G
⊢ Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹ = f ↔ f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f
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 g : ↑(coind' φ A)
hfg : ∀ (h : H), (Hom.hom f).toLinearMap (MonoidAlgebra.single h 1) = (Hom.hom g).toLinearMap (MonoidAlgebra.single h 1)
⊢ (Hom.hom f).toLinearMap = (Hom.hom g).toLinearMap

Tactic:
dsimp

Goal state after:
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 g : ↑(coind' φ A)
hfg : ∀ (h : H), (Hom.hom f).toLinearMap (MonoidAlgebra.single h 1) = (Hom.hom g).toLinearMap (MonoidAlgebra.single h 1)
⊢ (Hom.hom f).toLinearMap = (Hom.hom g).toLinearMap
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:
dsimp

Goal state after:
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)) ∘ₗ (Representation.ofMulAction k H H) (φ g) =
    A.ρ g ∘ₗ linearCombination k ↑f ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)
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
B : Rep k H
A : Rep k G
f : res φ B ⟶ A
g : H
⊢ LinearMap.codRestrict (Representation.coindV φ A.ρ) (LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h) ⋯ ∘ₗ
      B.ρ g =
    (Representation.coind φ A.ρ) g ∘ₗ
      LinearMap.codRestrict (Representation.coindV φ A.ρ) (LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h) ⋯

Tactic:
dsimp

Goal state after:
k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A✝ : Rep k G
B : Rep k H
A : Rep k G
f : res φ B ⟶ A
g : H
⊢ LinearMap.codRestrict (Representation.coindV φ A.ρ) ((LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h) ∘ₗ B.ρ g)
      ⋯ =
    (Representation.coind φ A.ρ) g ∘ₗ
      LinearMap.codRestrict (Representation.coindV φ A.ρ) (LinearMap.pi fun h ↦ (Hom.hom f).toLinearMap ∘ₗ B.ρ h) ⋯
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : CommRing k
G : Type u_2
inst✝⁹ : Group G
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module k[G] V
inst✝⁵ : IsScalarTower k k[G] V
W : Type u_4
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module k[G] W
inst✝¹ : IsScalarTower k k[G] W
π : W →ₗ[k] V
inst✝ : Fintype G
v : W
⊢ (equivariantProjection G π) v = (↑(Nat.card G))⁻¹ʳ • ∑ g, (π.conjugate g) v

Tactic:
simp only [equivariantProjection, smul_apply, sumOfConjugatesEquivariant_apply,
    Fintype.card_eq_nat_card]

Goal state after:
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝¹⁰ : CommRing k
G : Type u_2
inst✝⁹ : Group G
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : Module k[G] V
inst✝⁵ : IsScalarTower k k[G] V
W : Type u_4
inst✝⁴ : AddCommGroup W
inst✝³ : Module k W
inst✝² : Module k[G] W
inst✝¹ : IsScalarTower k k[G] W
π : W →ₗ[k] V
i : V →ₗ[k[G]] W
inst✝ : Fintype G
hcard : IsUnit ↑(Nat.card G)
h : ∀ (v : V), π (i v) = v
v : V
⊢ (equivariantProjection G π) (i v) = v

Tactic:
by
  rw [equivariantProjection_apply]
  simp only [conjugate_i π i h]
  rw [Finset.sum_const, Finset.card_univ, ← Nat.cast_smul_eq_nsmul k, smul_smul,
    Fintype.card_eq_nat_card, Ring.inverse_mul_cancel _ hcard, one_smul]

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

Goal state before:
pp: case insert
k : Type u
G : Type v
inst✝¹ : Semiring k
inst✝ : Monoid G
A B : Rep k G
ι : Type u'
f : ι → (A ⟶ B)
a : ι
s : Finset ι
ha : a ∉ s
h : Hom.hom (∑ i ∈ s, f i) = ∑ i ∈ s, Hom.hom (f i)
⊢ Hom.hom (∑ i ∈ insert a s, f i) = ∑ i ∈ insert a s, Hom.hom (f i)

Tactic:
| insert a s ha h =>

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

Goal state before:
pp: case insert
k : Type u
G : Type v
inst✝⁵ : Semiring k
inst✝⁴ : Monoid G
ι : Type u'
M N : Type v'
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module k M
inst✝ : Module k N
σ : Representation k G M
ρ : Representation k G N
f : ι → σ.IntertwiningMap ρ
a : ι
s : Finset ι
ha : a ∉ s
h : ofHom (∑ i ∈ s, f i) = ∑ i ∈ s, ofHom (f i)
⊢ ofHom (∑ i ∈ insert a s, f i) = ∑ i ∈ insert a s, ofHom (f i)

Tactic:
| insert a s ha h =>

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
H✝ : Type u_6
inst✝⁹ : Monoid H✝
π✝¹ : ContRepresentation R G✝ V
π' : ContRepresentation R H✝ W
G : Type u_7
H : Type u_8
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalSpace R
inst✝⁵ : ContinuousSMul R V
inst✝⁴ : ContinuousSMul R W
inst✝³ : Group H
inst✝² : TopologicalSpace H
φ : G →ₜ* H
π✝ : ContRepresentation R G V
inst✝¹ : IsTopologicalGroup G
inst✝ : IsTopologicalGroup H
π : ContRepresentation R G V
h1 h2 : H
⊢ {
      toFun := fun x ↦
        match x with
        | ⟨f, hf⟩ => ⟨f.comp (ContinuousMap.mulRight (h1 * h2)), ⋯⟩,
      map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } =
    {
        toFun := fun x ↦
          match x with
          | ⟨f, hf⟩ => ⟨f.comp (ContinuousMap.mulRight h1), ⋯⟩,
        map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } *
      {
        toFun := fun x ↦
          match x with
          | ⟨f, hf⟩ => ⟨f.comp (ContinuousMap.mulRight h2), ⋯⟩,
        map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

Tactic:
by ext; simp [ContinuousMap.mulRight_mul]

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
⊢ coinvariantsTensorIndHom φ A B ≫ coinvariantsTensorIndInv φ A B = 𝟙 (((coinvariantsTensor k H).obj (ind φ A)).obj B)

Tactic:
by
    ext h a b
    simpa [coinvariantsTensorIndInv, coinvariantsTensorMk,
      coinvariantsTensorIndHom, Coinvariants.mk_eq_iff] using
        Coinvariants.mem_ker_of_eq h (IndV.mk φ _ h a ⊗ₜ[k] b) _ <| by simp

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ ((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G) ≫
      (HomologicalComplex.singleMapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ) 0).hom.app
        (trivial k G k) =
    (forget₂ToModuleCatHomotopyEquiv k G).hom

Tactic:
dsimp

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ ((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G) ≫
      (HomologicalComplex.singleMapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ) 0).hom.app
        (trivial k G k) =
    (forget₂ToModuleCatHomotopyEquiv k G).hom
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
r : k
x : ↑A
g : G
⊢ (A.ρ g) (r • x) - r • x = ((RingHom.id k) r • fun g ↦ (A.ρ g) x - x) g

Tactic:
dsimp

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
r : k
x : ↑A
g : G
⊢ (A.ρ g) (r • x) - r • x = r • ((A.ρ g) x - x)
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 y : G → ↑A
g : G × G
⊢ (A.ρ g.1) ((x + y) g.2) - (x + y) (g.1 * g.2) + (x + y) g.1 =
    ((fun g ↦ (A.ρ g.1) (x g.2) - x (g.1 * g.2) + x g.1) + fun g ↦ (A.ρ g.1) (y g.2) - y (g.1 * g.2) + y g.1) g

Tactic:
dsimp

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : G → ↑A
g : G × G
⊢ (A.ρ g.1) (x g.2 + y g.2) - (x (g.1 * g.2) + y (g.1 * g.2)) + (x g.1 + y g.1) =
    (A.ρ g.1) (x g.2) - x (g.1 * g.2) + x g.1 + ((A.ρ g.1) (y g.2) - y (g.1 * g.2) + y g.1)
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
r : k
x : G → ↑A
g : G × G
⊢ (A.ρ g.1) ((r • x) g.2) - (r • x) (g.1 * g.2) + (r • x) g.1 =
    ((RingHom.id k) r • fun g ↦ (A.ρ g.1) (x g.2) - x (g.1 * g.2) + x g.1) g

Tactic:
dsimp

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
r : k
x : G → ↑A
g : G × G
⊢ (A.ρ g.1) (r • x g.2) - r • x (g.1 * g.2) + r • x g.1 = r • ((A.ρ g.1) (x g.2) - x (g.1 * g.2) + x g.1)
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 y : G × G → ↑A
g : G × G × G
⊢ (A.ρ g.1) ((x + y) (g.2.1, g.2.2)) - (x + y) (g.1 * g.2.1, g.2.2) + (x + y) (g.1, g.2.1 * g.2.2) -
      (x + y) (g.1, g.2.1) =
    ((fun g ↦ (A.ρ g.1) (x (g.2.1, g.2.2)) - x (g.1 * g.2.1, g.2.2) + x (g.1, g.2.1 * g.2.2) - x (g.1, g.2.1)) + fun g ↦
        (A.ρ g.1) (y (g.2.1, g.2.2)) - y (g.1 * g.2.1, g.2.2) + y (g.1, g.2.1 * g.2.2) - y (g.1, g.2.1))
      g

Tactic:
dsimp

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : G × G → ↑A
g : G × G × G
⊢ (A.ρ g.1) (x (g.2.1, g.2.2) + y (g.2.1, g.2.2)) - (x (g.1 * g.2.1, g.2.2) + y (g.1 * g.2.1, g.2.2)) +
        (x (g.1, g.2.1 * g.2.2) + y (g.1, g.2.1 * g.2.2)) -
      (x (g.1, g.2.1) + y (g.1, g.2.1)) =
    (A.ρ g.1) (x (g.2.1, g.2.2)) - x (g.1 * g.2.1, g.2.2) + x (g.1, g.2.1 * g.2.2) - x (g.1, g.2.1) +
      ((A.ρ g.1) (y (g.2.1, g.2.2)) - y (g.1 * g.2.1, g.2.2) + y (g.1, g.2.1 * g.2.2) - y (g.1, g.2.1))
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
r : k
x : G × G → ↑A
g : G × G × G
⊢ (A.ρ g.1) ((r • x) (g.2.1, g.2.2)) - (r • x) (g.1 * g.2.1, g.2.2) + (r • x) (g.1, g.2.1 * g.2.2) -
      (r • x) (g.1, g.2.1) =
    ((RingHom.id k) r • fun g ↦
        (A.ρ g.1) (x (g.2.1, g.2.2)) - x (g.1 * g.2.1, g.2.2) + x (g.1, g.2.1 * g.2.2) - x (g.1, g.2.1))
      g

Tactic:
dsimp

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
r : k
x : G × G → ↑A
g : G × G × G
⊢ (A.ρ g.1) (r • x (g.2.1, g.2.2)) - r • x (g.1 * g.2.1, g.2.2) + r • x (g.1, g.2.1 * g.2.2) - r • x (g.1, g.2.1) =
    r • ((A.ρ g.1) (x (g.2.1, g.2.2)) - x (g.1 * g.2.1, g.2.2) + x (g.1, g.2.1 * g.2.2) - x (g.1, g.2.1))
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 : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (A.ρ y.1) (x ((piFinTwoEquiv fun x ↦ G).symm (y.2.1, y.2.2))) -
          x ((piFinTwoEquiv fun x ↦ G).symm (y.1 * y.2.1, y.2.2)) +
        x ((piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1 * y.2.2)) -
      x ((piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1)) =
    (A.ρ (((Fin.consEquiv fun a ↦ G).symm.trans ((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G))).symm y 0))
        (x fun i ↦
          ((Fin.consEquiv fun a ↦ G).symm.trans ((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G))).symm y i.succ) +
      ∑ j,
        (-1) ^ (↑j + 1) •
          x
            (j.contractNth (fun x1 x2 ↦ x1 * x2)
              (((Fin.consEquiv fun a ↦ G).symm.trans ((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G))).symm y))

Tactic:
dsimp

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (A.ρ y.1) (x ((piFinTwoEquiv fun x ↦ G).symm (y.2.1, y.2.2))) -
          x ((piFinTwoEquiv fun x ↦ G).symm (y.1 * y.2.1, y.2.2)) +
        x ((piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1 * y.2.2)) -
      x ((piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1)) =
    (A.ρ ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y) 0))
        (x fun i ↦ (Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y) i.succ) +
      ∑ j,
        (-1) ^ (↑j + 1) •
          x
            (j.contractNth (fun x1 x2 ↦ x1 * x2)
              ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)))
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
a : A
⊢ IsBoundary₀ G a ↔ ∃ x, (x.sum fun g z ↦ g • z - z) = a

Tactic:
by
  constructor
  · rintro ⟨x, hx⟩
    use x.sum (fun g a => single g (-(g⁻¹ • a)))
    simp_all [sum_neg_index, sum_sum_index, neg_add_eq_sub]
  · rintro ⟨x, hx⟩
    use x.sum (fun g a => single g (-(g • a)))
    simp_all [sum_neg_index, sum_sum_index, neg_add_eq_sub]

Goal state after:
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
⊢ x ∈ maximalIdeal (AdicCompletion (maximalIdeal R) R) ↔ ↑x 1 = 0

Tactic:
have : (AdicCompletion.eval (maximalIdeal R) R 1).ker =
    (maximalIdeal R) • (⊤ : Submodule R (AdicCompletion (maximalIdeal R) R)) := by
    simp [← pow_smul_top_eq_ker_eval (maximalIdeal R).fg_of_isNoetherianRing]

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 (AdicCompletion (maximalIdeal R) R) ↔ ↑x 1 = 0
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_1
k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
⊢ (mapShortComplexH1 (g.comp f) (φ ≫ (resFunctor f).map ψ)).τ₁ = (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₁

Tactic:
{ simp only [shortComplexH1]
    ext
    simp [Prod.map]}

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

Goal state before:
pp: case refine_2
k : Type u
inst✝³ : CommRing k
G H K : Type u
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group K
A : Rep k G
B : Rep k H
C : Rep k K
f : G →* H
g : H →* K
φ : A ⟶ res f B
ψ : B ⟶ res g C
⊢ (mapShortComplexH1 (g.comp f) (φ ≫ (resFunctor f).map ψ)).τ₂ = (mapShortComplexH1 f φ ≫ mapShortComplexH1 g ψ).τ₂

Tactic:
{ simp only [shortComplexH1]
    ext
    simp [Prod.map]}

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

Goal state before:
pp: case lTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ map I.mkQ counit ∘ₗ comul = (TensorProduct.mk R (C ⧸ I) R).flip 1 ∘ₗ I.mkQ

Tactic:
rw [CoassocSimps.map_counit_comp_comul_right]; rfl

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

Goal state before:
pp: case refine_3
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ map ((AlgHom.id R (A ⧸ I)).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap) counit ∘ₗ comul =
    (↑(Algebra.TensorProduct.rid R R (A ⧸ I)).symm).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap

Tactic:
rw [CoassocSimps.map_counit_comp_comul_right]; rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_8
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R[M]
hx : IsGroupLikeElem R x
h : x ∉ Set.range fun x ↦ single x 1
this✝ : LinearIndepOn R id (insert x (Set.range fun x ↦ single x 1))
this : x.coeff.sum single ∉ span R (Set.range fun x ↦ single x 1)
g : M
hg : g ∈ x.coeff.support
⊢ single g (x.coeff g) ∈ span R (Set.range fun x ↦ single x 1)

Tactic:
rw [← mul_one (x.coeff g), ← smul_eq_mul, ← smul_single]

Goal state after:
R : Type u_1
M : Type u_8
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R[M]
hx : IsGroupLikeElem R x
h : x ∉ Set.range fun x ↦ single x 1
this✝ : LinearIndepOn R id (insert x (Set.range fun x ↦ single x 1))
this : x.coeff.sum single ∉ span R (Set.range fun x ↦ single x 1)
g : M
hg : g ∈ x.coeff.support
⊢ x.coeff g • single g 1 ∈ span R (Set.range fun x ↦ single x 1)
Module: Mathlib.RingTheory.Bialgebra.MonoidAlgebra

Goal state before:
pp: case single_one_right
R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : R[G] →ₐc[R] R[H]
x : G
⊢ (mapDomainBialgHom R (mapDomainOfBialgHom f)) (single x 1) = f (single x 1)

pp: case single_one_left
R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : R[G] →ₐc[R] R[H]
⊢ (↑(mapDomainBialgHom R (mapDomainOfBialgHom f))).comp singleOneAlgHom = (↑f).comp singleOneAlgHom

Tactic:
· rw [mapDomainBialgHom_single]
    exact single_mapDomainOfBialgHomFun_one f x

Goal state after:
case single_one_left
R : Type u_1
G : Type u_5
H : Type u_6
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Group H
f : R[G] →ₐc[R] R[H]
⊢ (↑(mapDomainBialgHom R (mapDomainOfBialgHom f))).comp singleOneAlgHom = (↑f).comp singleOneAlgHom
Module: Mathlib.RingTheory.Regular.LinearMap

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
⊢ ∃ p ∈ associatedPrimes R M, annihilator R N ≤ p

Tactic:
rcases associatedPrimes.nonempty R M with ⟨Ia, hIa⟩

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
Ia : Ideal R
hIa : Ia ∈ associatedPrimes R M
⊢ ∃ p ∈ associatedPrimes R M, annihilator R N ≤ p