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

Goal state before:
pp: case pos
Ω : 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
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

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

Goal state after:
case pos
Ω : 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
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case pos
Ω : 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) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
⊢ Tendsto (fun n ↦ eLpNorm (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω - ∫ (x : Ω), X 0 x ∂μ) p μ) atTop (𝓝 0)

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

Goal state after:
case pos
Ω : 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) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
⊢ Tendsto (fun n ↦ eLpNorm (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω - ∫ (x : Ω), X 0 x ∂μ) p μ) atTop (𝓝 0)
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: case ofMonoidHom
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
π₂ : ContRepresentation R G V
toMonoidHom✝ : G →* V →L[R] V
x✝ : (fun π ↦ ⇑π.toMonoidHom) { toMonoidHom := toMonoidHom✝ } = (fun π ↦ ⇑π.toMonoidHom) π₂
⊢ { toMonoidHom := toMonoidHom✝ } = π₂

Tactic:
cases π₂

Goal state after:
case ofMonoidHom.ofMonoidHom
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
toMonoidHom✝¹ toMonoidHom✝ : G →* V →L[R] V
x✝ :
  (fun π ↦ ⇑π.toMonoidHom) { toMonoidHom := toMonoidHom✝¹ } = (fun π ↦ ⇑π.toMonoidHom) { toMonoidHom := toMonoidHom✝ }
⊢ { toMonoidHom := toMonoidHom✝¹ } = { toMonoidHom := toMonoidHom✝ }
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝² x✝¹ x✝ : Rep k G
⊢ (α_ x✝² x✝¹ x✝).hom ≫ (mkIso (Representation.TensorProduct.comm x✝².ρ (x✝¹ ⊗ x✝).ρ)).hom ≫ (α_ x✝¹ x✝ x✝²).hom =
    (mkIso (Representation.TensorProduct.comm x✝².ρ x✝¹.ρ)).hom ▷ x✝ ≫
      (α_ x✝¹ x✝² x✝).hom ≫ x✝¹ ◁ (mkIso (Representation.TensorProduct.comm x✝².ρ x✝.ρ)).hom

Tactic:
ext : 2

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
x✝² x✝¹ x✝ : Rep k G
⊢ (Hom.hom
        ((α_ x✝² x✝¹ x✝).hom ≫
          (mkIso (Representation.TensorProduct.comm x✝².ρ (x✝¹ ⊗ x✝).ρ)).hom ≫ (α_ x✝¹ x✝ x✝²).hom)).toLinearMap =
    (Hom.hom
        ((mkIso (Representation.TensorProduct.comm x✝².ρ x✝¹.ρ)).hom ▷ x✝ ≫
          (α_ x✝¹ x✝² x✝).hom ≫ x✝¹ ◁ (mkIso (Representation.TensorProduct.comm x✝².ρ x✝.ρ)).hom)).toLinearMap
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y Z : Rep k G
⊢ (α_ X Y Z).inv ≫ (mkIso (Representation.TensorProduct.comm (X ⊗ Y).ρ Z.ρ)).hom ≫ (α_ Z X Y).inv =
    X ◁ (mkIso (Representation.TensorProduct.comm Y.ρ Z.ρ)).hom ≫
      (α_ X Z Y).inv ≫ (mkIso (Representation.TensorProduct.comm X.ρ Z.ρ)).hom ▷ Y

Tactic:
ext : 2

Goal state after:
k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y Z : Rep k G
⊢ (Hom.hom
        ((α_ X Y Z).inv ≫ (mkIso (Representation.TensorProduct.comm (X ⊗ Y).ρ Z.ρ)).hom ≫ (α_ Z X Y).inv)).toLinearMap =
    (Hom.hom
        (X ◁ (mkIso (Representation.TensorProduct.comm Y.ρ Z.ρ)).hom ≫
          (α_ X Z Y).inv ≫ (mkIso (Representation.TensorProduct.comm X.ρ Z.ρ)).hom ▷ Y)).toLinearMap
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case h₀
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
f : ↑(coind.{u, v, v, w} S.subtype A)
hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g
⊢ ∀ b ∈ Finset.univ, b ≠ ⟦g⟧ → b.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑f g)) ⋯ = 0

Tactic:
intro b _ hb

Goal state after:
case h₀
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
f : ↑(coind.{u, v, v, w} S.subtype A)
hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g
b : Quotient (QuotientGroup.rightRel S)
a✝ : b ∈ Finset.univ
hb : b ≠ ⟦g⟧
⊢ b.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑f g)) ⋯ = 0
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case h₀.h
k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
S : Subgroup G
A : Rep.{w, u, v} k ↥S
inst✝ : S.FiniteIndex
g : G
f : ↑(coind.{u, v, v, w} S.subtype A)
hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g
b : G
a✝ : ⟦b⟧ ∈ Finset.univ
hb : ⟦b⟧ ≠ ⟦g⟧
⊢ ⟦b⟧.liftOn (fun g ↦ (IndV.mk S.subtype A.ρ g) (↑f g)) ⋯ = 0

Tactic:
| h b =>

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
g : ↑(coind.{u, v, v, w} S.subtype A)
a : G
⊢ ↑(A.indToCoind (A.coindToInd g)) a = ↑g a

Tactic:
conv_lhs => rw [coindToInd_apply]

Goal state after:
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
g : ↑(coind.{u, v, v, w} S.subtype A)
a : G
⊢ ↑(A.indToCoind (∑ g_1, g_1.liftOn (fun g_2 ↦ (IndV.mk S.subtype A.ρ g_2) (↑g g_2)) ⋯)) a = ↑g a
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality

Goal state before:
pp: k : Type u
G : Type v
inst✝⁴ : Ring k
inst✝³ : TopologicalSpace k
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
i : ℕ
⊢ (cochainsMap (ContinuousMonoidHom.id G) (𝟙 X)).f i = (𝟙 X.homogeneousCochains).f i

Tactic:
cochainsMap_f,

Goal state after:
k : Type u
G : Type v
inst✝⁴ : Ring k
inst✝³ : TopologicalSpace k
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
i : ℕ
⊢ invariantsResMap (↑(ContinuousMonoidHom.id G)) (resolutionMap (ContinuousMonoidHom.id G) (𝟙 X) (i + 1)) =
    (𝟙 X.homogeneousCochains).f i
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case h₀
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
g : ↑(coind.{u, v, v, w} S.subtype A)
a : G
⊢ ∀ b ∈ Finset.univ, b ≠ ⟦a⟧ → ↑(A.indToCoind (b.liftOn (fun g_1 ↦ (IndV.mk S.subtype A.ρ g_1) (↑g g_1)) ⋯)) a = 0

Tactic:
intro b _ hb

Goal state after:
case h₀
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
g : ↑(coind.{u, v, v, w} S.subtype A)
a : G
b : Quotient (QuotientGroup.rightRel S)
a✝ : b ∈ Finset.univ
hb : b ≠ ⟦a⟧
⊢ ↑(A.indToCoind (b.liftOn (fun g_1 ↦ (IndV.mk S.subtype A.ρ g_1) (↑g g_1)) ⋯)) a = 0
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case h₀.h
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
g : ↑(coind.{u, v, v, w} S.subtype A)
a b : G
a✝ : ⟦b⟧ ∈ Finset.univ
hb : ⟦b⟧ ≠ ⟦a⟧
⊢ ↑(A.indToCoind (⟦b⟧.liftOn (fun g_1 ↦ (IndV.mk S.subtype A.ρ g_1) (↑g g_1)) ⋯)) a = 0

Tactic:
| h b =>

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

Goal state before:
pp: case refine_1.zero
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
⊢ (fun gv ↦ (ρ gv.1) gv.2 - gv.2) ((fun x ↦ g ^ x) 0, α) ∈ ↑(ρ g - LinearMap.id).range

Tactic:
exact ⟨0, by simp⟩

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

Goal state before:
pp: case refine_2
k : Type u_1
G : Type u_2
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
this✝ : Fintype G
x : MonoidAlgebra k G
hx : x ∈ ((linearCombination k fun x ↦ 1) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)).ker
this : x = x.coeff.sum fun g r ↦ MonoidAlgebra.single g r - MonoidAlgebra.single 1 r
⊢ (x.coeff.sum fun g r ↦ MonoidAlgebra.single g r - MonoidAlgebra.single 1 r) ∈ Coinvariants.ker (leftRegular k G)

Tactic:
exact Submodule.finsuppSum_mem _ _ _ _ fun g _ =>
      Coinvariants.mem_ker_of_eq g (.single 1 (x.coeff g)) _ (by simp)

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n : ℕ
C : ↑(groupCohomology A n) → Prop
x : ↑(groupCohomology A n)
h : ∀ (x : ↑(cocycles A n)), C ((ConcreteCategory.hom (π A n)) x)
⊢ C x

Tactic:
rcases (ModuleCat.epi_iff_surjective (π A n)).1 inferInstance x with ⟨y, rfl⟩
  exact h y

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

Goal state before:
pp: case h
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
this : aux f z = ∑ h, ↑(f h) * h z
g : Gal(L/K)
⊢ g • (Units.mk0 (aux f z) hz)⁻¹ / (Units.mk0 (aux f z) hz)⁻¹ = f g

Tactic:
simp only [IsMulCocycle₁, AlgEquiv.smul_units_def,
    map_inv, div_inv_eq_mul, inv_mul_eq_iff_eq_mul, Units.ext_iff, this,
    Units.val_mul, Units.coe_map, Units.val_mk0, MonoidHom.coe_coe] at hf ⊢

Goal state after:
case h
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ˣ
z : L
hz : aux f z ≠ 0
this : aux f z = ∑ h, ↑(f h) * h z
g : Gal(L/K)
hf : ∀ (g h : Gal(L/K)), ↑(f (g * h)) = g ↑(f h) * ↑(f g)
⊢ ∑ h, ↑(f h) * h z = g (∑ h, ↑(f h) * h z) * ↑(f g)
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
X✝ Y✝ : SimplexCategoryᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ (cechNerveTerminalFrom G).map x✝ ≫ (Types.productIso fun x ↦ G).hom =
    (Types.productIso fun x ↦ G).hom ≫ (classifyingSpaceUniversalCover G ⋙ forget (Action (Type u) G)).map x✝

Tactic:
ext : 2

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
X✝ Y✝ : SimplexCategoryᵒᵖ
x✝ : X✝ ⟶ Y✝
⊢ (ConcreteCategory.hom ((cechNerveTerminalFrom G).map x✝ ≫ (Types.productIso fun x ↦ G).hom)).toFun =
    (ConcreteCategory.hom
        ((Types.productIso fun x ↦ G).hom ≫
          (classifyingSpaceUniversalCover G ⋙ forget (Action (Type u) G)).map x✝)).toFun
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Monoid G
⊢ (Arrow.mk (terminal.from G)).augmentedCechNerve ≅ compForgetAugmented G

Tactic:
exact
    Comma.isoMk (CechNerveTerminalFrom.iso G ≪≫ cechNerveTerminalFromIsoCompForget G)
      (Iso.refl _) (by ext : 1; exact IsTerminal.hom_ext terminalIsTerminal _ _)

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
j : ℕ
⊢ (diagonalSuccIsoFree k G (j + 1)).symm.hom ≫ (standardComplex k G).d (j + 1) j =
    d k G j ≫ (diagonalSuccIsoFree k G j).symm.hom

Tactic:
Iso.symm_hom,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
j : ℕ
⊢ (diagonalSuccIsoFree k G (j + 1)).inv ≫ (standardComplex k G).d (j + 1) j =
    d k G j ≫ (diagonalSuccIsoFree k G j).symm.hom
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
j : ℕ
⊢ (diagonalSuccIsoFree k G (j + 1)).inv ≫ (standardComplex k G).d (j + 1) j =
    d k G j ≫ (diagonalSuccIsoFree k G j).symm.hom

Tactic:
Iso.symm_hom,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
j : ℕ
⊢ (diagonalSuccIsoFree k G (j + 1)).inv ≫ (standardComplex k G).d (j + 1) j = d k G j ≫ (diagonalSuccIsoFree k G j).inv
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; rw [map_smul, smul_sub]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n : ℕ
C : ↑(groupHomology A n) → Prop
x : ↑(groupHomology A n)
h : ∀ (x : ↑(cycles A n)), C ((ConcreteCategory.hom (π A n)) x)
⊢ C x

Tactic:
rcases (ModuleCat.epi_iff_surjective (π A n)).1 inferInstance x with ⟨y, rfl⟩
  exact h y

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

Goal state before:
pp: k G A : Type u
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
f : G → A
hf : f ∈ coboundaries₁ (Rep.ofDistribMulAction k G A)
⊢ IsCoboundary₁ f

Tactic:
rcases hf with ⟨a, rfl⟩

Goal state after:
k G A : Type u
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
a : ↑(ModuleCat.of k ↑(Rep.ofDistribMulAction k G A))
⊢ IsCoboundary₁ ((ModuleCat.Hom.hom (d₀₁ (Rep.ofDistribMulAction k G A))) a)
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G A : Type u
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
f : G × G → A
hf : f ∈ coboundaries₂ (Rep.ofDistribMulAction k G A)
⊢ IsCoboundary₂ f

Tactic:
rcases hf with ⟨a, rfl⟩

Goal state after:
k G A : Type u
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
a : ↑(ModuleCat.of k (G → ↑(Rep.ofDistribMulAction k G A)))
⊢ IsCoboundary₂ ((ModuleCat.Hom.hom (d₁₂ (Rep.ofDistribMulAction k G A))) a)
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 : ↥(cocycles₁ A)
⊢ (ModuleCat.Hom.hom ((cochainsIso₁ A).inv ≫ (inhomogeneousCochains A).d 1 (1 + 1))) ⇑x = 0

Tactic:
eq_d₁₂_comp_inv,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₁ A)
⊢ (ModuleCat.Hom.hom (d₁₂ A ≫ (cochainsIso₂ A).inv)) ⇑x = 0
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 : G →* H
φ✝ : res f A ⟶ B
n✝ n : ℕ
X Y : Rep k H
φ : X ⟶ Y
⊢ (functor k H n).map φ ≫ map f (𝟙 (res f Y)) n = map f (𝟙 (res f X)) n ≫ (resFunctor f ⋙ functor k G n).map φ

Tactic:
simp only [functor_map, Functor.comp_map,
      ← cancel_epi (groupCohomology.π _ n), HomologicalComplex.homologyπ_naturality_assoc,
      HomologicalComplex.homologyπ_naturality, ← HomologicalComplex.cyclesMap_comp_assoc,
      ← cochainsMap_comp, res_obj_ρ, Category.comp_id]
    rfl

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
⊢ (ConcreteCategory.hom (d₁₀ A)) (single g a) = (A.ρ g⁻¹) a - a

Tactic:
by
  simp [d₁₀]

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
a : ↑A
⊢ (ConcreteCategory.hom (d₁₀ A)) (single 1 a) = 0

Tactic:
by
  simp [d₁₀]

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
⊢ (ConcreteCategory.hom (d₁₀ A)) (single g⁻¹ a) = -(ConcreteCategory.hom (d₁₀ A)) (single g ((A.ρ g) a))

Tactic:
by
  simp [d₁₀]

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
⊢ (ModuleCat.Hom.hom (d₁₀ A)).ker = ⊤

Tactic:
d₁₀_eq_zero_of_isTrivial,

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ (ModuleCat.Hom.hom 0).ker = ⊤
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 × G
a : ↑A
⊢ single g a ∈ cycles₂ A ↔ single (g.1 * g.2) ((A.ρ g.1) a) = single g.2 a + single g.1 ((A.ρ g.1) a)

Tactic:
rw [← (mapRange_injective (α := G) _ (map_zero _) (A.ρ.apply_bijective g.1⁻¹).1).eq_iff]
  simp [mem_cycles₂_iff, mapRange_add, eq_comm]

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

Goal state before:
pp: case pos.refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : (Ideal.map constantCoeff I).FG
⊢ (insert X (⇑C '' generators (Ideal.map constantCoeff I))).Finite

pp: case pos.refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : (Ideal.map constantCoeff I).FG
⊢ (⇑C '' generators (Ideal.map constantCoeff I)).ncard + 1 ≤ spanFinrank (Ideal.map constantCoeff I) + 1

Tactic:
· simpa using! Set.Finite.map _ (FG.finite_generators hfg)

Goal state after:
case pos.refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : (Ideal.map constantCoeff I).FG
⊢ (⇑C '' generators (Ideal.map constantCoeff I)).ncard + 1 ≤ spanFinrank (Ideal.map constantCoeff I) + 1
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case mp
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
h : ∀ (n : ℕ), IsOpen[inst✝¹] ↑(⊥ ^ n)
_h' : ∀ s ∈ 𝓝 0, ∃ n, ↑(⊥ ^ n) ⊆ s
⊢ DiscreteTopology A

Tactic:
rw [discreteTopology_iff_isOpen_singleton_zero]

Goal state after:
case mp
A : Type u_2
inst✝² : CommRing A
inst✝¹ : TopologicalSpace A
inst✝ : IsTopologicalRing A
h : ∀ (n : ℕ), IsOpen[inst✝¹] ↑(⊥ ^ n)
_h' : ∀ s ∈ 𝓝 0, ∃ n, ↑(⊥ ^ n) ⊆ s
⊢ IsOpen[inst✝¹] {0}
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
⊢ IsAdicComplete (maximalIdeal (AdicCompletion (maximalIdeal R) R)) (AdicCompletion (maximalIdeal R) R)

Tactic:
rw [AdicCompletion.maximalIdeal_eq_map_of_fg fg]
  exact AdicCompletion.isAdicComplete_self _ fg

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : CommSemiring T
inst✝¹ : Algebra R S
inst✝ : Algebra S T
x✝¹ x✝ : R[X]
z : S
⊢ (algebraMap S T) ((aeval z) (x✝¹ * x✝)) =
    ((fun z ↦ (algebraMap S T) ((aeval z) x✝¹)) * fun z ↦ (algebraMap S T) ((aeval z) x✝)) z

Tactic:
by simp only [Pi.mul_apply, map_mul]

Goal state after:
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
x : ↥(cycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (A.quotientToCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.quotientToCoinvariants S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.quotientToCoinvariants S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S))) x)
z : ↥(cycles₁ (res S.subtype (A.toCoinvariants S)))
hz :
  (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype (A.toCoinvariants S))))) z) =
    (ConcreteCategory.hom (H1π (A.toCoinvariants S)))
      ((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
w : ↑(ModuleCat.of k (G × G →₀ ↑(A.toCoinvariants S)))
hzw :
  (ModuleCat.Hom.hom (d₂₁ (A.toCoinvariants S))) w =
    ↑((ConcreteCategory.hom (mapCycles₁ S.subtype (𝟙 (res S.subtype (A.toCoinvariants S))))) z) -
      ↑((ConcreteCategory.hom (mapCycles₁ (MonoidHom.id G) (A.toCoinvariantsMkQ S))) x)
Z : ↥S →₀ ↑A
hZ : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ Z = ↑z
W : G × G →₀ ↑A
hW : mapRange ⇑(Coinvariants.mk (MonoidHom.comp A.ρ S.subtype)) ⋯ W = w
b : G →₀ ↑A := ↑x + (ConcreteCategory.hom (d₂₁ A)) W - (lmapDomain (↑A) k ⇑S.subtype) Z
hb : ∀ (g : G), b g ∈ Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)
β : G →₀ ↥(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)) :=
  mapRange (Function.invFun ⇑(Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype) ⋯ b
hβb : mapRange Subtype.val ⋯ β = b
⊢ β ∈ ⊤

Tactic:
by trivial

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

Goal state before:
pp: R : Type u_1
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group I
f : R[H] →ₐc[R] R[I]
g : R[G] →ₐc[R] R[H]
⊢ mapDomainOfBialgHom (f.comp g) =
    mapDomainOfBialgHom (mapDomainBialgHom R ((mapDomainOfBialgHom f).comp (mapDomainOfBialgHom g)))

Tactic:
mapDomainBialgHom_comp,

Goal state after:
R : Type u_1
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group I
f : R[H] →ₐc[R] R[I]
g : R[G] →ₐc[R] R[H]
⊢ mapDomainOfBialgHom (f.comp g) =
    mapDomainOfBialgHom
      ((mapDomainBialgHom R (mapDomainOfBialgHom f)).comp (mapDomainBialgHom R (mapDomainOfBialgHom g)))