mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Equiv

Goal state before:
pp: k : Type u
inst✝⁸ : Semiring k
G : Type v
inst✝⁷ : Monoid G
V : Type v'
inst✝⁶ : AddCommMonoid V
inst✝⁵ : Module k V
W : Type w'
inst✝⁴ : AddCommMonoid W
inst✝³ : Module k W
H : Type w
inst✝² : Subsingleton H
inst✝¹ : MulOneClass H
inst✝ : MulAction G H
g : G
⊢ ↑(MonoidAlgebra.uniqueLinearEquiv k H) ∘ₗ (ofMulAction k G H) g =
    (trivial k G k) g ∘ₗ ↑(MonoidAlgebra.uniqueLinearEquiv k H)

Tactic:
ext a; simp [Subsingleton.elim (g • a) a]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case e_f.e_a
Ω : 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 : ℕ
⊢ Var[S (u i); ℙ] = ∑ j ∈ range (u i), Var[Y j; ℙ]

Tactic:
hS,

Goal state after:
case e_f.e_a
Ω : 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 : ℕ
⊢ Var[(fun n ↦ ∑ i ∈ range n, Y i) (u i); ℙ] = ∑ j ∈ range (u i), Var[Y j; ℙ]
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
⊢ 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 =
    ((((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)

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

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
ρ : Representation k G V
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : V
hv : v ∈ ρ.invariants
⊢ ρ.averageMap v = v

Tactic:
rw [mem_invariants] at hv

Goal state after:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
ρ : Representation k G V
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : V
hv : ∀ (g : G), (ρ g) v = v
⊢ ρ.averageMap v = v
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun x ↦ max x 0
neg : ℝ → ℝ := fun x ↦ max (-x) 0
posm : Measurable pos
negm : Measurable neg
A : ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))
B : ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))
ω : Ω
hωpos : Tendsto (fun n ↦ (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))
hωneg : Tendsto (fun n ↦ (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))
⊢ Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
convert! hωpos.sub hωneg using 2

Goal state after:
case e'_3
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun x ↦ max x 0
neg : ℝ → ℝ := fun x ↦ max (-x) 0
posm : Measurable pos
negm : Measurable neg
A : ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))
B : ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))
ω : Ω
hωpos : Tendsto (fun n ↦ (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))
hωneg : Tendsto (fun n ↦ (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))
x✝ : ℕ
⊢ (∑ i ∈ range x✝, X i ω) / ↑x✝ = (∑ i ∈ range x✝, (pos ∘ X i) ω) / ↑x✝ - (∑ i ∈ range x✝, (neg ∘ X i) ω) / ↑x✝

case e'_5
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ¬∀ᵐ (ω : Ω), X 0 ω = 0
this : IsProbabilityMeasure μ
pos : ℝ → ℝ := fun x ↦ max x 0
neg : ℝ → ℝ := fun x ↦ max (-x) 0
posm : Measurable pos
negm : Measurable neg
A : ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))
B : ∀ᵐ (ω : Ω), Tendsto (fun n ↦ (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))
ω : Ω
hωpos : Tendsto (fun n ↦ (∑ i ∈ range n, (pos ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (pos ∘ X 0) a))
hωneg : Tendsto (fun n ↦ (∑ i ∈ range n, (neg ∘ X i) ω) / ↑n) atTop (𝓝 (∫ (a : Ω), (neg ∘ X 0) a))
⊢ ∫ (x : Ω), X 0 x ∂μ = (∫ (a : Ω), (pos ∘ X 0) a) - ∫ (a : Ω), (neg ∘ X 0) a
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
x✝¹ x✝ : H
⊢ {
      toFun := fun f ↦
        (resFunctor φ).map (↑(leftRegular k H).leftRegularHomEquiv.symm (MonoidAlgebra.single (x✝¹ * x✝) 1)) ≫ f,
      map_add' := ⋯, map_smul' := ⋯ } =
    {
        toFun := fun f ↦
          (resFunctor φ).map (↑(leftRegular k H).leftRegularHomEquiv.symm (MonoidAlgebra.single x✝¹ 1)) ≫ f,
        map_add' := ⋯, map_smul' := ⋯ } *
      {
        toFun := fun f ↦
          (resFunctor φ).map (↑(leftRegular k H).leftRegularHomEquiv.symm (MonoidAlgebra.single x✝ 1)) ≫ f,
        map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext
    simp [homEquiv, mul_assoc]

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.InjectiveProjective

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : IsSemisimpleRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X Y : Type u_2
x✝⁴ : AddCommGroup X
x✝³ : AddCommGroup Y
x✝² : Module R X
x✝¹ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] M
h : Y →ₗ[R] M
comp : h ∘ₗ f = g
x✝ : X
⊢ h (f x✝) = g x✝

Tactic:
rw [← comp, LinearMap.comp_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
g g₁ : G
a : ↑A
s : ↥S
⊢ (A.indToCoindAux g) a (↑s * g₁) = (A.ρ s) ((A.indToCoindAux g) a g₁)

Tactic:
by
  rcases em ((QuotientGroup.rightRel S).r g₁ g) with ⟨s₁, rfl⟩ | h
  · simp only [indToCoindAux, LinearMap.pi_apply]
    rw [dif_pos ⟨s * s₁, mul_assoc ..⟩, dif_pos ⟨s₁, rfl⟩]
    simp [S.1.smul_def, mul_assoc, ← S.1.mul_def]
  · rw [indToCoindAux_of_not_rel _ _ _ h, indToCoindAux_of_not_rel, map_zero]
    exact mt (fun ⟨s₁, hs₁⟩ => ⟨s⁻¹ * s₁, by simp_all [S.1.smul_def, mul_assoc]⟩) h

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case inl.e_6
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
g₁ : G
a : ↑A
s s₁ : ↥S
⊢ ⟨s₁ • g₁ * (↑s * g₁)⁻¹, ⋯⟩ * s = ⟨s₁ • g₁ * g₁⁻¹, ⋯⟩

Tactic:
simp [Subtype.ext_iff, S.1.smul_def, mul_assoc]

Goal state after:
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case inl
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
g₁ : G
a : ↑A
s s₁ : ↥S
⊢ (A.indToCoindAux (↑s * g₁)) ((A.ρ s) a) ((fun m ↦ m • g₁) s₁) = (A.indToCoindAux g₁) a ((fun m ↦ m • g₁) s₁)

pp: case inr
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
g₁ g₂ : G
a : ↑A
s : ↥S
h : ¬(QuotientGroup.rightRel S) g₂ g₁
⊢ (A.indToCoindAux (↑s * g₁)) ((A.ρ s) a) g₂ = (A.indToCoindAux g₁) a g₂

Tactic:
· simp only [indToCoindAux, LinearMap.pi_apply]
    rw [dif_pos ⟨s₁ * s⁻¹, by simp [S.1.smul_def, smul_eq_mul, mul_assoc]⟩, dif_pos ⟨s₁, rfl⟩,
      ← Module.End.mul_apply, ← map_mul]
    congr
    simp [Subtype.ext_iff, S.1.smul_def, mul_assoc]

Goal state after:
case inr
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
g₁ g₂ : G
a : ↑A
s : ↥S
h : ¬(QuotientGroup.rightRel S) g₂ g₁
⊢ (A.indToCoindAux (↑s * g₁)) ((A.ρ s) a) g₂ = (A.indToCoindAux g₁) a g₂
Module: Mathlib.RepresentationTheory.FiniteIndex

Goal state before:
pp: case inr.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
g₁ g₂ : G
a : ↑A
s : ↥S
h : ¬(QuotientGroup.rightRel S) g₂ g₁
⊢ ¬(QuotientGroup.rightRel S) g₂ (↑s * g₁)

Tactic:
exact mt (fun ⟨s₁, hs₁⟩ => ⟨s₁ * s, by simp_all [S.1.smul_def, mul_assoc]⟩) h

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

Goal state before:
pp: case zero.right
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ Epi
    ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).map
        ((((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv (trivial k G k)).symm
          ⟨(trivial k G k).leftRegularHom 1, ⋯⟩)).τ₂

Tactic:
rw [Rep.epi_iff_surjective]

Goal state after:
case zero.right
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
⊢ Function.Surjective
    ⇑(Hom.hom
        ((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).map
            ((((chainComplexFunctor k g).obj (leftRegular k G)).toSingle₀Equiv (trivial k G k)).symm
              ⟨(trivial k G k).leftRegularHom 1, ⋯⟩)).τ₂)
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
⊢ inhomogeneousCochains A ≅ (barComplex k G).linearYonedaObj k A

Tactic:
refine HomologicalComplex.Hom.isoOfComponents
    (fun i ↦ (Rep.freeLiftLEquiv k G (Fin i → G) A).toModuleIso.symm) ?_

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
⊢ ∀ (i j : ℕ),
    (ComplexShape.up ℕ).Rel i j →
      (freeLiftLEquiv k G (Fin i → G) A).toModuleIso.symm.hom ≫ ((barComplex k G).linearYonedaObj k A).d i j =
        (inhomogeneousCochains A).d i j ≫ (freeLiftLEquiv k G (Fin j → G) A).toModuleIso.symm.hom
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
eq3 :
  MonoidAlgebra.single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) 1 =
    MonoidAlgebra.single (Fin.partialProd i ∘ Fin.succ) 1
H :
  ∀ (m : ℕ) (f : Fin m → G) (g : G) (r : k),
    (Hom.hom (diagonalSuccIsoFree k G m).inv) (single f (MonoidAlgebra.single g r)) =
      MonoidAlgebra.single (g • Fin.partialProd f) r
⊢ (Hom.hom (diagonalSuccIsoFree k G n).inv) (single (fun i_1 ↦ i i_1.succ) (MonoidAlgebra.single (i 0) 1)) +
      ∑ x,
        (Hom.hom (diagonalSuccIsoFree k G n).inv)
          (single (x.contractNth (fun x1 x2 ↦ x1 * x2) i) (MonoidAlgebra.single 1 ((-1) ^ (↑x + 1)))) =
    (Hom.hom ((standardComplex k G).d (n + 1) n))
      ((Hom.hom (diagonalSuccIsoFree k G (n + 1)).inv) (single i (MonoidAlgebra.single 1 1)))

Tactic:
simp only [H, one_smul]

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
eq3 :
  MonoidAlgebra.single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) 1 =
    MonoidAlgebra.single (Fin.partialProd i ∘ Fin.succ) 1
H :
  ∀ (m : ℕ) (f : Fin m → G) (g : G) (r : k),
    (Hom.hom (diagonalSuccIsoFree k G m).inv) (single f (MonoidAlgebra.single g r)) =
      MonoidAlgebra.single (g • Fin.partialProd f) r
⊢ MonoidAlgebra.single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) 1 +
      ∑ x, MonoidAlgebra.single (Fin.partialProd (x.contractNth (fun x1 x2 ↦ x1 * x2) i)) ((-1) ^ (↑x + 1)) =
    (Hom.hom ((standardComplex k G).d (n + 1) n)) (MonoidAlgebra.single (Fin.partialProd i) 1)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic

Goal state before:
pp: k✝ G✝ : Type u
inst✝⁴ : CommRing k✝
inst✝³ : Group G✝
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
n : ℕ
inst✝ : DecidableEq G
⊢ inhomogeneousChains A ≅ HomologicalComplex.coinvariantsTensorObj A (barComplex k G)

Tactic:
by
  refine HomologicalComplex.Hom.isoOfComponents ?_ ?_
  · intro i
    apply (coinvariantsTensorFreeLEquiv A (Fin i → G)).toModuleIso.symm
  rintro i j rfl
  simp [d_eq, -LinearEquiv.toModuleIso_hom, -LinearEquiv.toModuleIso_inv]

Goal state after:
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 2 (2 + 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.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ π A 1 ≫ (H1Iso A).hom = (isoCocycles₁ A).hom ≫ (shortComplexH1 A).moduleCatLeftHomologyData.π

Tactic:
simp [H1Iso, isoCocycles₁, π, HomologicalComplex.homologyπ, leftHomologyπ]

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ (inhomogeneousCochains A).d 0 1 = 0

Tactic:
ext; simp [inhomogeneousCochains.d, Unique.eq_default (α := Fin 0 → G),
      CochainComplex.of.d]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.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
⊢ (H1InfRes A S).Exact

Tactic:
moduleCat_exact_iff_ker_sub_range

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
⊢ (ModuleCat.Hom.hom (H1InfRes A S).g).ker ≤ (ModuleCat.Hom.hom (H1InfRes A S).f).range
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a : R
ha : a ≠ 0
ha₂ : ¬↑(span {a}) ∩ ↑(closure {r | Prime r}).toSubsemigroup = ∅
x : R
hx : x ∈ ↑(span {a})
hx₂ : x ∈ ↑(closure {r | Prime r}).toSubsemigroup
b : R
hb : b * a = x
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a

Tactic:
← hb,

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a : R
ha : a ≠ 0
ha₂ : ¬↑(span {a}) ∩ ↑(closure {r | Prime r}).toSubsemigroup = ∅
x : R
hx : x ∈ ↑(span {a})
b : R
hx₂ : b * a ∈ ↑(closure {r | Prime r}).toSubsemigroup
hb : b * a = x
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : closure {r | Prime r} ≤ closure {r | IsUnit r ∨ Prime r}
z : R
h : IsUnit z
⊢ (∀ b ∈ ∅, Prime b) ∧ Associated ∅.prod z

Tactic:
simpa using (associated_one_iff_isUnit.2 h).symm

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : ¬I.FG
⊢ spanFinrank I ≤ spanFinrank (Ideal.map constantCoeff I) + 1

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

Tactic:
· exact spanFinrank_of_not_fg hfg ▸ Nat.zero_le _

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
hI : X ∈ I
hfg : I.FG
⊢ spanFinrank I ≤ spanFinrank (Ideal.map constantCoeff I) + 1
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
J : Ideal R⟦X⟧
hJI : J ≤ I
hXI : X ∉ I
hJ : J.FG
h' : Ideal.map constantCoeff I ≤ Ideal.map constantCoeff J
⊢ I ≤ J

Tactic:
replace h' := h'.antisymm (Ideal.map_mono hJI)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
J : Ideal R⟦X⟧
hJI : J ≤ I
hXI : X ∉ I
hJ : J.FG
h' : Ideal.map constantCoeff I = Ideal.map constantCoeff J
⊢ I ≤ J
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
hfg : ¬P.FG
⊢ spanFinrank P ≤ spanFinrank (Ideal.map constantCoeff P) + 1

pp: case pos
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
hfg : P.FG
⊢ spanFinrank P ≤ spanFinrank (Ideal.map constantCoeff P) + 1

Tactic:
· exact spanFinrank_of_not_fg hfg ▸ Nat.zero_le _

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
hfg : P.FG
⊢ spanFinrank P ≤ spanFinrank (Ideal.map constantCoeff P) + 1
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case pos
R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(x = 0 ∧ k = 1)
h3 : k = 1
⊢ 0 = if x = 0 then 1 else 0

Tactic:
if_neg (by tauto)

Goal state after:
case pos
R : Type u_2
inst✝ : CommSemiring R
n k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(x = 0 ∧ k = 1)
h3 : k = 1
⊢ 0 = 0
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
j : Fin n
k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(x = single j 1 ∧ k = 0)
h3 : k = 0
⊢ 0 = if x = single j 1 then 1 else 0

Tactic:
if_neg (by tauto)

Goal state after:
case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
j : Fin n
k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(x = single j 1 ∧ k = 0)
h3 : k = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(k = 0 ∧ x = 0)
h3 : k = 0
⊢ 0 = if x = 0 then r else 0

Tactic:
if_neg (by tauto)

Goal state after:
case pos
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
k : ℕ
x : Fin n →₀ ℕ
h1 : ¬(k = 0 ∧ x = 0)
h3 : k = 0
⊢ 0 = 0
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_1
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
⊢ (mapShortComplexH1 f 0).τ₁ = Hom.τ₁ 0

Tactic:
{

Goal state after:
case refine_1
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
⊢ (mapShortComplexH1 f 0).τ₁ = Hom.τ₁ 0
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_2
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
⊢ (mapShortComplexH1 f 0).τ₂ = Hom.τ₂ 0

Tactic:
{

Goal state after:
case refine_2
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
⊢ (mapShortComplexH1 f 0).τ₂ = Hom.τ₂ 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:
{

Goal state after:
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 ψ).τ₁
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:
{

Goal state after:
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 ψ).τ₂
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : I.FG
x : ℕ → AdicCompletion I M
m n : ℕ
hx : (eval I M m) (x m - x n) = 0
h' : m ≤ n
⊢ ↑(x n) m = ↑(x m) m

Tactic:
_root_.map_sub,

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : I.FG
x : ℕ → AdicCompletion I M
m n : ℕ
hx : (eval I M m) (x m) - (eval I M m) (x n) = 0
h' : m ≤ n
⊢ ↑(x n) m = ↑(x m) m
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_1
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
⊢ (mapShortComplexH2 f 0).τ₁ = Hom.τ₁ 0

Tactic:
{

Goal state after:
case refine_1
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
⊢ (mapShortComplexH2 f 0).τ₁ = Hom.τ₁ 0
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case refine_2
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
⊢ (mapShortComplexH2 f 0).τ₂ = Hom.τ₂ 0

Tactic:
{

Goal state after:
case refine_2
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
⊢ (mapShortComplexH2 f 0).τ₂ = Hom.τ₂ 0