mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ι
ω : Ω
⊢ stoppedProcess (fun i ↦ {ω | ⊥ < min (hL.localSeq n ω) (τ n (nk n) ω)}.indicator (X i))
      (fun ω ↦ min (hL.localSeq n ω) (τ n (nk n) ω)) i ω =
    stoppedProcess
      (fun i ↦
        {ω | ⊥ < τ n (nk n) ω}.indicator
          (stoppedProcess (fun i ↦ {ω | ⊥ < hL.localSeq n ω}.indicator (X i)) (hL.localSeq n) i))
      (τ n (nk n)) i ω

Tactic:
rw [stoppedProcess_indicator_comm', stoppedProcess_indicator_comm',
    stoppedProcess_stoppedProcess, stoppedProcess_indicator_comm']

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 : ι
ω : Ω
⊢ (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 ω
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case ha
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := ⋯
ρ : Measure ℝ := ⋯
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
k : ℕ
a✝ : k ∈ range K
⊢ 0 ≤ ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ

Tactic:
refine intervalIntegral.integral_nonneg_of_forall ?_ fun u => sq_nonneg _

Goal state after:
case ha
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
k : ℕ
a✝ : k ∈ range K
⊢ ↑k ≤ ↑(k + 1)
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
X : Type w
g : G
⊢ (linearize k G (Action.trivial G X)) g = LinearMap.id

Tactic:
ext (x : X) : 2
  rw [LinearMap.comp_apply, LinearMap.id_comp, MonoidAlgebra.lsingle_apply, linearize_single]
  simp only [Action.trivial_ρ]
  rfl

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 : (forget₂ (FDRep R G) (Rep R G)).obj X ⟶ (forget₂ (FDRep R G) (Rep R G)).obj Y
g : G
⊢ ModuleCat.Hom.hom (X.ρ g ≫ InducedCategory.homMk (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap)).hom =
    ModuleCat.Hom.hom (InducedCategory.homMk (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap) ≫ Y.ρ g).hom

Tactic:
simp only [FGModuleCat.obj_carrier]

Goal state after:
R k : Type u
G : Type v
inst✝² : CommRing R
inst✝¹ : Field k
inst✝ : Monoid G
X Y : FDRep R G
f : (forget₂ (FDRep R G) (Rep R G)).obj X ⟶ (forget₂ (FDRep R G) (Rep R G)).obj Y
g : G
⊢ ModuleCat.Hom.hom (X.ρ g ≫ InducedCategory.homMk (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap)).hom =
    ModuleCat.Hom.hom (InducedCategory.homMk (ModuleCat.ofHom (Rep.Hom.hom f).toLinearMap) ≫ Y.ρ g).hom
Module: Mathlib.RepresentationTheory.Rep.Iso

Goal state before:
pp: k : Type u
G✝ : Type v
inst✝² : CommRing k
inst✝¹ : Monoid G✝
G : Type u
inst✝ : Group G
n : ℕ
⊢ Projective (diagonal k G (n + 1))

Tactic:
by
  exact Projective.of_iso (diagonalSuccIsoFree k G n).symm inferInstance

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.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
⊢ Tendsto (fun n ↦ eLpNorm (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω - ∫ (x : Ω), X 0 x ∂μ) p μ) atTop (𝓝 0)

Tactic:
by
  -- First exclude the trivial case where the space is not a probability space
  by_cases h : ∀ᵐ ω ∂μ, X 0 ω = 0
  · have I : ∀ᵐ ω ∂μ, ∀ i, X i ω = 0 := by
      rw [ae_all_iff]
      intro i
      exact (hident i).symm.ae_snd (p := fun x ↦ x = 0) measurableSet_eq h
    have A (n : ℕ) : eLpNorm (fun ω => (n : ℝ)⁻¹ • (∑ i ∈ range n, X i ω) - μ[X 0]) p μ = 0 := by
      simp only [integral_eq_zero_of_ae h, sub_zero]
      apply eLpNorm_eq_zero_of_ae_zero
      filter_upwards [I] with ω hω
      simp [hω]
    simp [A]
  -- Then use ae convergence and uniform integrability
  have : IsProbabilityMeasure μ := MemLp.isProbabilityMeasure_of_indepFun
    (X 0) (X 1) (zero_lt_one.trans_le hp).ne' hp' hℒp h (hindep zero_ne_one)
  have hmeas : ∀ i, AEStronglyMeasurable (X i) μ := fun i =>
    (hident i).aestronglyMeasurable_iff.2 hℒp.1
  have hint : Integrable (X 0) μ := hℒp.integrable hp
  have havg (n : ℕ) :
      AEStronglyMeasurable (fun ω => (n : ℝ)⁻¹ • (∑ i ∈ range n, X i ω)) μ :=
    AEStronglyMeasurable.const_smul (aestronglyMeasurable_fun_sum _ fun i _ => hmeas i) _
  refine tendsto_Lp_finite_of_tendstoInMeasure hp hp' havg (memLp_const _) ?_
    (tendstoInMeasure_of_tendsto_ae havg (strong_law_ae _ hint hindep hident))
  rw [(_ : (fun (n : ℕ) ω => (n : ℝ)⁻¹ • (∑ i ∈ range n, X i ω))
            = fun (n : ℕ) => (n : ℝ)⁻¹ • (∑ i ∈ range n, X i))]
  · apply UniformIntegrable.unifIntegrable
    apply uniformIntegrable_average hp
    exact MemLp.uniformIntegrable_of_identDistrib hp hp' hℒp hident
  · ext n ω
    simp only [Pi.smul_apply, Finset.sum_apply]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Basic

Goal state before:
pp: 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
i : ℕ
σ : ↑(X.homogeneousCochains.X i).toModuleCat
⊢ ↑((TopModuleCat.Hom.hom (X.homogeneousCochains.d i (i + 1))) σ) = (Hom.hom (X.d (i + 1))) ↑σ

Tactic:
by
  rw [homogeneousCochains.d_eq]
  dsimp [ContIntertwiningMap.mapInvariants_apply]

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)
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
X✝ Y✝ : Rep.{max u w, u, v} k ↥S
f : X✝ ⟶ Y✝
g1 : G
x : ↑X✝
g2 : G
⊢ ↑(((AlgebraTensorModule.curry
                ((Hom.hom ((indFunctor k S.subtype).map f ≫ Y✝.indCoindIso.hom)).toLinearMap ∘ₗ
                  Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) X✝.ρ)) ∘ₗ
              MonoidAlgebra.lsingle g1)
            1)
          x)
      g2 =
    ↑(((AlgebraTensorModule.curry
                ((Hom.hom (X✝.indCoindIso.hom ≫ (coindFunctor k S.subtype).map f)).toLinearMap ∘ₗ
                  Coinvariants.mk (tprod (MonoidHom.comp (Representation.leftRegular k G) S.subtype) X✝.ρ)) ∘ₗ
              MonoidAlgebra.lsingle g1)
            1)
          x)
      g2

Tactic:
simp [indToCoind, indMap, indToCoindAux_comm]

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

Goal state before:
pp: case a.a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| ((barComplex k G).linearYonedaObj k A).d n (n + 1) ≫
    𝟙 (((barComplex k G).linearYonedaObj k A).X (n + 1)) ≫ ((barComplex k G).linearYonedaObj k A).d (n + 1) (n + 1 + 1)

pp: case a.a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A).toModuleIso.hom

pp: case a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| (freeLiftLEquiv k G (Fin n → G) A).toModuleIso.inv

Tactic:
rw [Category.id_comp, ((barComplex k G).linearYonedaObj k A).d_comp_d]

Goal state after:
case a.a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| 0

case a.a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A).toModuleIso.hom

case a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| (freeLiftLEquiv k G (Fin n → G) A).toModuleIso.inv
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
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1) ∘ₗ
            TensorProduct.map (A.ρ s) (B.ρ (φ s))))
        x)
      y =
    ((TensorProduct.AlgebraTensorModule.curry
          (TensorProduct.lift ((ind φ A).coinvariantsTensorMk B ∘ₗ IndV.mk φ A.ρ 1)))
        x)
      y

Tactic:
simpa [Coinvariants.mk_eq_iff, coinvariantsTensorMk] using
      Coinvariants.mem_ker_of_eq (φ s) (IndV.mk φ A.ρ (1 : H) x ⊗ₜ[k] y) _ <| by
      simp [← Coinvariants.mk_inv_tmul]

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : Gal(L/K) → Lˣ
hf : IsMulCocycle₁ f
⊢ IsMulCoboundary₁ f

Tactic:
obtain ⟨z, hz⟩ : ∃ z, aux f z ≠ 0 :=
    not_forall.1 (fun H => aux_ne_zero f <| funext <| fun x => H x)

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : Gal(L/K) → Lˣ
hf : IsMulCocycle₁ f
z : L
hz : aux f z ≠ 0
⊢ IsMulCoboundary₁ f
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 : ℕ
h₀ : NeZero i
hi : Even i
⊢ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap = 0

Tactic:
by ext; simp [sub_hom,
    Rep.applyAsHom, Rep.norm]

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
⊢ ModuleCat.ofHom (Hom.hom A.norm).toLinearMap ≫ ModuleCat.ofHom (Hom.hom (A.applyAsHom g - 𝟙 A)).toLinearMap = 0

Tactic:
by ext; simp [sub_hom,
    Rep.applyAsHom, Rep.norm]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
z : ↥(cycles₁ X.X₃)
y : G →₀ ↑X.X₂
hy : (mapRange.linearMap (Rep.Hom.hom X.g).toLinearMap) y = ↑z
x : ↑X.X₁
hx : (Rep.Hom.hom X.f) x = (ConcreteCategory.hom (d₁₀ X.X₂)) y
x✝ : Fin 0 → G
⊢ ((mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) ((ConcreteCategory.hom (chainsIso₀ X.X₁).inv) x)) x✝ =
    ((ModuleCat.Hom.hom (d₁₀ X.X₂ ≫ (chainsIso₀ X.X₂).inv)) y) x✝

Tactic:
simp [chainsIso₀, ← hx]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
X Y : Rep R G
f g : X ⟶ Y
⊢ map (f + g) = map f + map g

Tactic:
ext (i | i) : 1

Goal state after:
case ofNat
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
X Y : Rep R G
f g : X ⟶ Y
i : ℕ
⊢ (map (f + g)).f (Int.ofNat i) = (map f + map g).f (Int.ofNat i)

case negSucc
R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
X Y : Rep R G
f g : X ⟶ Y
i : ℕ
⊢ (map (f + g)).f (Int.negSucc i) = (map f + map g).f (Int.negSucc i)
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: case h
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx : (ConcreteCategory.hom (H1π A)) x ∈ (ModuleCat.Hom.hom (H1InfRes A S).g).ker
⊢ (ConcreteCategory.hom (H1π A)) x ∈ (ModuleCat.Hom.hom (H1InfRes A S).f).range

Tactic:
simp_all only [H1InfRes_X₂, H1InfRes_X₃, H1InfRes_g, H1InfRes_X₁, LinearMap.mem_ker,
    H1π_comp_map_apply S.subtype, H1InfRes_f]

Goal state after:
case h
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
⊢ (ConcreteCategory.hom (H1π A)) x ∈
    (ModuleCat.Hom.hom (map (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) 1)).range
Module: Mathlib.RingTheory.Noetherian.OfPrime

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
H : ∀ (I : Ideal R), I.IsPrime → I.FG
⊢ IsNoetherianRing R

Tactic:
refine ⟨isOka_fg.forall_of_forall_prime' (fun C hC₁ hC₂ I hI h ↦ ⟨sSup C, ?_, h⟩) H⟩
  obtain ⟨G, hG⟩ := h
  obtain ⟨J, J_mem_C, G_subset_J⟩ : ∃ J ∈ C, (G : Set R) ⊆ J := by
    refine hC₂.directedOn.exists_mem_subset_of_finset_subset_biUnion ⟨I, hI⟩ (fun _ hx ↦ ?_)
    simp only [Set.mem_iUnion, SetLike.mem_coe, exists_prop]
    exact (Submodule.mem_sSup_of_directed ⟨I, hI⟩ hC₂.directedOn).1 <| hG ▸ subset_span hx
  suffices J_eq_sSup : J = sSup C from J_eq_sSup ▸ J_mem_C
  exact le_antisymm (le_sSup J_mem_C) (hG ▸ Ideal.span_le.2 G_subset_J)

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
inst✝ : A.IsTrivial
⊢ LinearMap.ker 0 = ⊤

Tactic:
LinearMap.ker_zero

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ ⊤ = ⊤
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
x✝¹ : G
x✝ : ↑A
⊢ (((fun f ↦ f.comp ↑(cycles₁IsoOfIsTrivial A).symm.toLinearEquiv.toAddEquiv)
            (((fun f ↦ f.comp ↑(H1Iso A).symm.toLinearEquiv.toAddEquiv)
                  (TensorProduct.lift (mkH1OfIsTrivial A) ∘ₗ H1ToTensorOfIsTrivial A).toAddMonoidHom).comp
              (QuotientAddGroup.mk' (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup))).comp
        (singleAddHom x✝¹))
      x✝ =
    (((fun f ↦ f.comp ↑(cycles₁IsoOfIsTrivial A).symm.toLinearEquiv.toAddEquiv)
            (((fun f ↦ f.comp ↑(H1Iso A).symm.toLinearEquiv.toAddEquiv) LinearMap.id.toAddMonoidHom).comp
              (QuotientAddGroup.mk' (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup))).comp
        (singleAddHom x✝¹))
      x✝

Tactic:
simp only [H1ToTensorOfIsTrivial, Iso.toLinearEquiv, AddMonoidHom.coe_comp,
          LinearMap.toAddMonoidHom_coe, LinearMap.coe_comp, AddMonoidHom.coe_toIntLinearMap]

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
x✝¹ : G
x✝ : ↑A
⊢ (((((⇑(TensorProduct.lift (mkH1OfIsTrivial A)) ∘
                ⇑(QuotientAddGroup.lift (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup
                      ((Finsupp.liftAddHom fun g ↦
                            ↑((TensorProduct.mk ℤ (Additive (Abelianization G)) ↑A)
                                (Additive.ofMul (Abelianization.of g)))).comp
                        (cycles₁ A).toAddSubgroup.subtype)
                      ⋯) ∘
                  ⇑↑(ModuleCat.Hom.hom (H1Iso A).hom)) ∘
              ⇑↑(LinearEquiv.ofLinearMap (ModuleCat.Hom.hom (H1Iso A).symm.hom) (ModuleCat.Hom.hom (H1Iso A).symm.inv) ⋯
                      ⋯).toAddEquiv) ∘
            ⇑(QuotientAddGroup.mk' (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup)) ∘
          ⇑↑(LinearEquiv.ofLinearMap (ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).symm.hom)
                  (ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).symm.inv) ⋯ ⋯).toAddEquiv) ∘
        ⇑(singleAddHom x✝¹))
      x✝ =
    ((((⇑LinearMap.id ∘
              ⇑↑(LinearEquiv.ofLinearMap (ModuleCat.Hom.hom (H1Iso A).symm.hom) (ModuleCat.Hom.hom (H1Iso A).symm.inv) ⋯
                      ⋯).toAddEquiv) ∘
            ⇑(QuotientAddGroup.mk' (shortComplexH1 A).moduleCatToCycles.range.toAddSubgroup)) ∘
          ⇑↑(LinearEquiv.ofLinearMap (ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).symm.hom)
                  (ModuleCat.Hom.hom (cycles₁IsoOfIsTrivial A).symm.inv) ⋯ ⋯).toAddEquiv) ∘
        ⇑(singleAddHom x✝¹))
      x✝
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)) = (coeff x) p

Tactic:
rw [← coeff_truncTotal _ hx, ← sub_eq_zero, ← MvPolynomial.coeff_sub]

Goal state after:
σ : 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
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
φ : A ⟶ res 1 B
x : ↑(ModuleCat.of k ↥(cycles₁ A))
⊢ ↑((ModuleCat.Hom.hom (mapCycles₁ 1 φ)) x) ∈ boundaries₁ B

Tactic:
simpa [coe_mapCycles₁ _ φ x, mapDomain, map_finsuppSum] using
    (boundaries₁ B).finsuppSum_mem k x.1 _ fun _ _ => single_one_mem_boundaries₁ (A := B) _

Goal state after:
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 : G →* H
φ : A ⟶ res f B
n : ℕ
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x✝ : G ⧸ S →₀ ↑(A.ofQuotient S)
hx : x✝ ∈ cycles₁ (A.ofQuotient S)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), ↑(s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
x y : G ⧸ S
h : s x = s y
⊢ x = y

Tactic:
← hs x,

Goal state after:
k G H : Type u
inst✝⁴ : CommRing k
inst✝³ : Group G
inst✝² : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x✝ : G ⧸ S →₀ ↑(A.ofQuotient S)
hx : x✝ ∈ cycles₁ (A.ofQuotient S)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), ↑(s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
x y : G ⧸ S
h : s x = s y
⊢ ↑(s x) = y
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
⊢ Submodule.comap
      (ModuleCat.Hom.hom
        ((mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f).τ₂ ≫ (shortComplexH1 A).pOpcycles))
      (ModuleCat.Hom.hom
          ((mapShortComplexH1 S.subtype (𝟙 (res S.subtype A))).τ₂ ≫ (shortComplexH1 A).pOpcycles)).range =
    ⊤

Tactic:
by
  rw [eq_top_iff]
  intro x _
  rcases mapRange_surjective _ (map_zero _) (chains₁ToCoinvariantsKer_surjective
    (res S.subtype A)) x with ⟨(X : G →₀ S →₀ A), hX⟩
  let Y : S →₀ A := X.sum fun g f =>
    mapRange.linearMap (A.ρ g⁻¹) (lmapDomain _ k (fun s => MulAut.conjNormal g⁻¹ s) f) - f
  let Z : G × G →₀ A := X.sum fun g f =>
    lmapDomain _ k (fun s => (g, g⁻¹ * s.1 * g)) f - lmapDomain _ k (fun s => (s.1, g)) f
  use Y
  apply (moduleCat_pOpcycles_eq_iff _ _ _).2 ⟨Z, ?_⟩
  change d₂₁ A Z = mapRange id rfl (lmapDomain _ k Subtype.val Y) -
    mapRange.linearMap (Submodule.subtype _) (mapDomain id x)
  simpa [map_finsuppSum, mapDomain, map_sub, ← hX, sum_single_index, curryLinearEquiv,
    curryEquiv, Finsupp.uncurry, d₂₁, Y, Z, sum_mapRange_index,
    chains₁ToCoinvariantsKer, d₁₀, single_sum, mul_assoc, sub_add_eq_add_sub,
    sum_sum_index, add_smul, sub_sub_sub_eq, lsingle, singleAddHom] using add_comm _ _

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
x✝ : Aᵐᵒᵖ
⊢ (map (↑(opLinearEquiv R)) (map (↑(opLinearEquiv R)) LinearMap.id))
      ((TensorProduct.assoc R A A Aᵐᵒᵖ)
        ((map (comul ∘ₗ ↑(opLinearEquiv R).symm ∘ₗ ↑(opLinearEquiv R))
            (LinearMap.id ∘ₗ LinearMap.id ∘ₗ ↑(opLinearEquiv R)))
          (comul ((opLinearEquiv R).symm x✝)))) =
    (map (↑(opLinearEquiv R))
        (map ↑(opLinearEquiv R) ↑(opLinearEquiv R) ∘ₗ comul ∘ₗ ↑(opLinearEquiv R).symm ∘ₗ ↑(opLinearEquiv R)))
      (comul ((opLinearEquiv R).symm x✝))

Tactic:
← lTensor_comp_rTensor

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
x✝ : Aᵐᵒᵖ
⊢ (lTensor Aᵐᵒᵖ (lTensor Aᵐᵒᵖ LinearMap.id ∘ₗ rTensor Aᵐᵒᵖ ↑(opLinearEquiv R)) ∘ₗ
        rTensor (A ⊗[R] Aᵐᵒᵖ) ↑(opLinearEquiv R))
      ((TensorProduct.assoc R A A Aᵐᵒᵖ)
        ((lTensor (A ⊗[R] A) (LinearMap.id ∘ₗ LinearMap.id ∘ₗ ↑(opLinearEquiv R)) ∘ₗ
            rTensor A (comul ∘ₗ ↑(opLinearEquiv R).symm ∘ₗ ↑(opLinearEquiv R)))
          (comul ((opLinearEquiv R).symm x✝)))) =
    (lTensor Aᵐᵒᵖ
          ((lTensor Aᵐᵒᵖ ↑(opLinearEquiv R) ∘ₗ rTensor A ↑(opLinearEquiv R)) ∘ₗ
            comul ∘ₗ ↑(opLinearEquiv R).symm ∘ₗ ↑(opLinearEquiv R)) ∘ₗ
        rTensor A ↑(opLinearEquiv R))
      (comul ((opLinearEquiv R).symm x✝))
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
p : Ideal R
hp : p ∈ (annihilator R M).minimalPrimes
prime : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
⊢ Nontrivial (LocalizedModule p.primeCompl M)

Tactic:
simpa [← Module.mem_support_iff (p := ⟨p, prime⟩), Module.support_eq_zeroLocus] using! hp.1.2

Goal state after: