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

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊
ω : Ω
hω : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
h'ω : (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n
⊢ Tendsto (fun x ↦ (∑ i ∈ range ⌊c ^ x⌋₊, X i ω) / ↑⌊c ^ x⌋₊ - ∫ (a : Ω), X 0 a) atTop (𝓝 0)

Tactic:
← Asymptotics.isLittleO_one_iff ℝ

Goal state after:
Ω : 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
H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊
ω : Ω
hω : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
h'ω : (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n
⊢ (fun x ↦ (∑ i ∈ range ⌊c ^ x⌋₊, X i ω) / ↑⌊c ^ x⌋₊ - ∫ (a : Ω), X 0 a) =o[atTop] fun _x ↦ 1
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: G : Type u_1
k : Type u_2
V : Type u_3
inst✝³ : Group G
inst✝² : Field k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
ρ : Representation k G V
g h : G
⊢ ρ.character (h * g * h⁻¹) = ρ.character g

Tactic:
by
  rw [char_mul_comm, inv_mul_cancel_left]

Goal state after:
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: k : Type u
inst✝¹ : Field k
G : Type v
inst✝ : Group G
V : FDRep k G
g h : G
⊢ V.character (h * g * h⁻¹) = V.character g

Tactic:
by
  rw [char_mul_comm, inv_mul_cancel_left]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case neg
Ω : 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
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
have negm : Measurable neg := measurable_id'.neg.max measurable_const

Goal state after:
case neg
Ω : 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
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
⊢ ofHom { toLinearMap := (Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype, isIntertwining' := ⋯ } ≫
      A.toCoinvariantsMkQ S =
    0

Tactic:
by ext x; exact (Submodule.Quotient.mk_eq_zero _).2 x.2

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
π : ContRepresentation R G V
π' : ContRepresentation R G W
f : π →ⁱL π'
⊢ ∀ x ∈ π.invariants, f.toContinuousLinearMap x ∈ π'.invariants

Tactic:
by
    simp +contextual [f.toContinuousLinearMap_apply, ← f.isIntertwining]

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
φ : H →* G
f : π.restrict φ →ⁱL π'
⊢ ∀ x ∈ π.invariants, f.toContinuousLinearMap x ∈ π'.invariants

Tactic:
by
    simp +contextual [f.toContinuousLinearMap_apply, ← f.isIntertwining]

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

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

Tactic:
ext1; simp [comm_comp_rTensor]

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

Goal state before:
pp: case succ
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 : ℕ
ih : resolutionMap (ContinuousMonoidHom.id G) (𝟙 X) i = 𝟙 (X.resolutionX i)
⊢ ofHom (coind₁ResMap (ContinuousMonoidHom.id G) (Hom.hom (resolutionMap (ContinuousMonoidHom.id G) (𝟙 X) i))) =
    𝟙 (X.resolutionX (i + 1))

Tactic:
ih

Goal state after:
case succ
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 : ℕ
ih : resolutionMap (ContinuousMonoidHom.id G) (𝟙 X) i = 𝟙 (X.resolutionX i)
⊢ ofHom (coind₁ResMap (ContinuousMonoidHom.id G) (Hom.hom (𝟙 (X.resolutionX i)))) = 𝟙 (X.resolutionX (i + 1))
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality

Goal state before:
pp: case succ
k : Type u
G H K : Type v
inst✝¹⁰ : Ring k
inst✝⁹ : TopologicalSpace k
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalGroup H
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : IsTopologicalGroup K
X : TopRep k G
Y : TopRep k H
Z : TopRep k K
φ : H →ₜ* G
ψ : K →ₜ* H
f : res (↑φ) X ⟶ Y
g : res (↑ψ) Y ⟶ Z
i : ℕ
ih :
  resolutionMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) i =
    (resFunctor ↑ψ).map (resolutionMap φ f i) ≫ resolutionMap ψ g i
⊢ ofHom (coind₁ResMap (φ.comp ψ) (Hom.hom (resolutionMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) i))) =
    (resFunctor ↑ψ).map (ofHom (coind₁ResMap φ (Hom.hom (resolutionMap φ f i)))) ≫
      ofHom (coind₁ResMap ψ (Hom.hom (resolutionMap ψ g i)))

Tactic:
ih

Goal state after:
case succ
k : Type u
G H K : Type v
inst✝¹⁰ : Ring k
inst✝⁹ : TopologicalSpace k
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : IsTopologicalGroup H
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : IsTopologicalGroup K
X : TopRep k G
Y : TopRep k H
Z : TopRep k K
φ : H →ₜ* G
ψ : K →ₜ* H
f : res (↑φ) X ⟶ Y
g : res (↑ψ) Y ⟶ Z
i : ℕ
ih :
  resolutionMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) i =
    (resFunctor ↑ψ).map (resolutionMap φ f i) ≫ resolutionMap ψ g i
⊢ ofHom (coind₁ResMap (φ.comp ψ) (Hom.hom ((resFunctor ↑ψ).map (resolutionMap φ f i) ≫ resolutionMap ψ g i))) =
    (resFunctor ↑ψ).map (ofHom (coind₁ResMap φ (Hom.hom (resolutionMap φ f i)))) ≫
      ofHom (coind₁ResMap ψ (Hom.hom (resolutionMap ψ g i)))
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree

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
x : ↑X
h : ContinuousMap.const G x ∈ (X.resolution'.X 0).ρ.invariants
⊢ ⟨ContinuousMap.const G x, h⟩ ∈ (↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker

Tactic:
LinearMap.mem_ker,

Goal state after:
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
x : ↑X
h : ContinuousMap.const G x ∈ (X.resolution'.X 0).ρ.invariants
⊢ ↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1)) ⟨ContinuousMap.const G x, h⟩ = 0
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree

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
x✝ : ↥(↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
x : C(G, ↑X)
hx' : x ∈ (X.resolution'.X 0).ρ.invariants
hx : ⟨x, hx'⟩ ∈ (↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
g : G
⊢ ↑↑((fun x ↦
              match x with
              | ⟨x, hx⟩ => ⟨⟨ContinuousMap.const G x, ⋯⟩, ⋯⟩)
            ((fun x ↦
                match x with
                | ⟨σ, hσ⟩ => ⟨↑σ 1, ⋯⟩)
              ⟨⟨x, hx'⟩, hx⟩))
      g =
    ↑↑⟨⟨x, hx'⟩, hx⟩ g

Tactic:
LinearMap.mem_ker,

Goal state after:
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
x✝ : ↥(↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
x : C(G, ↑X)
hx' : x ∈ (X.resolution'.X 0).ρ.invariants
hx✝ : ⟨x, hx'⟩ ∈ (↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker
hx : ↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1)) ⟨x, hx'⟩ = 0
g : G
⊢ ↑↑((fun x ↦
              match x with
              | ⟨x, hx⟩ => ⟨⟨ContinuousMap.const G x, ⋯⟩, ⋯⟩)
            ((fun x ↦
                match x with
                | ⟨σ, hσ⟩ => ⟨↑σ 1, ⋯⟩)
              ⟨⟨x, hx'⟩, hx✝⟩))
      g =
    ↑↑⟨⟨x, hx'⟩, hx✝⟩ g
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
hi : Odd i
⊢ (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev i) i

Tactic:
rcases hi with ⟨j, rfl⟩

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
A : Rep k G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
j : ℕ
⊢ (ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev (2 * j + 1)) (2 * j + 1)
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
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

Tactic:
f

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
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
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
i j : ℕ
y : (Fin i → G) → ↑X.X₂
x : (Fin j → G) → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d i j)) y
⊢ (ConcreteCategory.hom (inhomogeneousCochains.d X.X₁ j)) x = 0

Tactic:
by simpa [CochainComplex.of.d] using!
    ((map_cochainsFunctor_shortExact hX).d_eq_zero_of_f_eq_d_apply i j y x
      (by simpa using! hx) (j + 1))

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
i j : ℕ
hij : i + 1 = j
z : (Fin i → G) → ↑X.X₃
hz : (ConcreteCategory.hom ((inhomogeneousCochains X.X₃).d i j)) z = 0
y : (Fin i → G) → ↑X.X₂
hy : (ConcreteCategory.hom ((cochainsMap (MonoidHom.id G) X.g).f i)) y = z
x : (Fin j → G) → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d i j)) y
⊢ (ConcreteCategory.hom (inhomogeneousCochains.d X.X₃ i)) z = 0

Tactic:
by subst hij; simpa [CochainComplex.of.d] using! hz

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 : ℕ
inst✝ : DecidableEq G
a✝ : Fin (n + 1) → G
x✝ : ↑A
⊢ (ModuleCat.Hom.hom (d A n) ∘ₗ lsingle a✝) x✝ =
    (ModuleCat.Hom.hom
          ((A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G)).toModuleIso.inv ≫
            (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n ≫
              (A.coinvariantsTensorFreeLEquiv (Fin n → G)).toModuleIso.hom) ∘ₗ
        lsingle a✝)
      x✝

Tactic:
simp [d_single (k := k), TensorProduct.tmul_add, TensorProduct.tmul_sum,
    barComplex.d_single (k := k)]

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
⊢ coboundaries₁ A = ⊥

Tactic:
by
  simp_rw [coboundaries₁, d₀₁_eq_zero]
  exact LinearMap.range_eq_bot.2 rfl

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

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : Monoid G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G × G → M
hf : IsMulCocycle₂ f
g : G
⊢ f (1, g) = f (1, 1)

Tactic:
by
  simpa only [one_smul, one_mul, mul_one, mul_right_inj] using (hf 1 1 g).symm

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) ((ModuleCat.Hom.hom (d₂₃ A)) ⇑x) = 0

Tactic:
cocycles₂.d₂₃_apply x,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₂ A)
⊢ (ModuleCat.Hom.hom (cochainsIso₃ A).inv) 0 = 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
x : ↥(cocycles₁ A)
h :
  (shortComplexH1 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyData ≫
        (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyIso.hom =
    cyclesMap' (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyData.π ≫
        (HomologicalComplex.sc (inhomogeneousCochains A) 1).leftHomologyIso.hom
⊢ (ModuleCat.Hom.hom (shortComplexH1 A).moduleCatLeftHomologyData.π) x = 0 ↔ ⇑x ∈ coboundaries₁ A

Tactic:
simp [LinearMap.range_codRestrict, coboundaries₁, shortComplexH1, cocycles₁]

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
⊢ (ComplexShape.down ℕ).Rel i ((ComplexShape.down ℕ).next i)

Tactic:
rcases hi with ⟨j, rfl⟩

Goal state after:
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
j : ℕ
⊢ (ComplexShape.down ℕ).Rel (2 * j + 1) ((ComplexShape.down ℕ).next (2 * j + 1))
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
A : Rep k G
i : ℕ
hi : Odd i
x y : ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker
⊢ (ConcreteCategory.hom (groupHomologyπOdd A g hg i hi)) x = (ConcreteCategory.hom (groupHomologyπOdd A g hg i hi)) y ↔
    ↑x - ↑y ∈ LinearMap.range A.ρ.norm

Tactic:
rw [← sub_eq_zero, ← map_sub, groupHomologyπOdd_eq_zero_iff, AddSubgroupClass.coe_sub]

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
  · rfl
  · ext1
    simp only [CochainComplex.ConnectData.map_f, chainsMap_id_f_hom_eq_mapRange, Rep.add_hom,
      Representation.IntertwiningMap.add_toLinearMap, HomologicalComplex.add_f_apply,
      ModuleCat.hom_add]
    ext; simp

Goal state after:
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✝¹ x✝ : Rep k G
⊢ (functor k G n).map 0 = 0

Tactic:
by simp [map]

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

Goal state before:
pp: A : Type u_3
σ : Type u_4
inst✝ : CommRing A
I : Ideal (MvPolynomial σ A)
d : MvPolynomial σ A
⊢ (↑↑(Ideal.Quotient.mk I)).toFun d =
    eval₂ (algebraMap A (MvPolynomial σ A ⧸ I)) (fun d ↦ (Ideal.Quotient.mk I) (X d)) d

Tactic:
RingHom.toFun_eq_coe,

Goal state after:
A : Type u_3
σ : Type u_4
inst✝ : CommRing A
I : Ideal (MvPolynomial σ A)
d : MvPolynomial σ A
⊢ (Ideal.Quotient.mk I) d = eval₂ (algebraMap A (MvPolynomial σ A ⧸ I)) (fun d ↦ (Ideal.Quotient.mk I) (X d)) d
Module: Mathlib.RingTheory.PowerSeries.Ideal

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

Tactic:
exact spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_X_mem hP

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this✝ : (𝓝 0).IsCountablyGenerated
this : (𝓤 R).IsCountablyGenerated
H : CompleteSpace R
⊢ ∀ (f : ℕ → R), (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ L, ∀ (n : ℕ), f n - L ∈ I ^ n

Tactic:
f

Goal state after:
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this✝ : (𝓝 0).IsCountablyGenerated
this : (𝓤 R).IsCountablyGenerated
H : CompleteSpace R
f : ℕ → R
⊢ (∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m) → ∃ L, ∀ (n : ℕ), f n - L ∈ I ^ n
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : ¬optionElim n y = x
h3 : n = x none
h : y = x.some
⊢ False

Tactic:
absurd h1; ext u
      cases u <;> simp_all

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
y : AdicCompletion I ↥(I ^ n • ⊤)
⊢ (ofPowSMul I M n) y ∈ (eval I M n).ker

Tactic:
LinearMap.mem_ker,

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
y : AdicCompletion I ↥(I ^ n • ⊤)
⊢ (eval I M n) ((ofPowSMul I M n) y) = 0
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 : x m - x n ∈ (eval I M m).ker
h' : m ≤ n
⊢ ↑(x n) m = ↑(x m) m

Tactic:
LinearMap.mem_ker,

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 - x n) = 0
h' : m ≤ n
⊢ ↑(x n) m = ↑(x m) m
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.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
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S) (s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
z : G × G →₀ ↑A := (lmapDomain (↑A) k (Prod.map s s)) y
hz :
  (lmapDomain (↑A) k ⇑(QuotientGroup.mk' S)) ((ModuleCat.Hom.hom (d₂₁ A)) z) =
    (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y
v : G →₀ ↑A := x - (ModuleCat.Hom.hom (d₂₁ A)) z
hv : mapDomain (s ∘ QuotientGroup.mk) v = 0
e : G → G × G := fun g ↦ (s ↑g, (s ↑g)⁻¹ * g)
he : Function.Injective e
⊢ (ConcreteCategory.hom (H1π A)) ⟨x, hxc⟩ ∈ (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f).range

Tactic:
let ve : G × G →₀ A := mapDomain e v

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
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S) (s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
z : G × G →₀ ↑A := (lmapDomain (↑A) k (Prod.map s s)) y
hz :
  (lmapDomain (↑A) k ⇑(QuotientGroup.mk' S)) ((ModuleCat.Hom.hom (d₂₁ A)) z) =
    (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y
v : G →₀ ↑A := x - (ModuleCat.Hom.hom (d₂₁ A)) z
hv : mapDomain (s ∘ QuotientGroup.mk) v = 0
e : G → G × G := fun g ↦ (s ↑g, (s ↑g)⁻¹ * g)
he : Function.Injective e
ve : G × G →₀ ↑A := mapDomain e v
⊢ (ConcreteCategory.hom (H1π A)) ⟨x, hxc⟩ ∈ (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f).range
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
⊢ (map f p).contentIdeal = Ideal.map f p.contentIdeal

Tactic:
suffices span ((map f p).coeffs ∪ {0}) = span (f '' p.coeffs ∪ {0}) by
    simpa [contentIdeal_def, map_span]
  congr 1
  ext s
  by_cases hs : s = 0
  · simp [hs]
  · aesop (add simp mem_coeffs_iff)

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

Goal state before:
pp: R : Type u_1
A : Type u_3
G : Type u_5
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
⊢ Submodule.span A (Set.range fun y ↦ single y 1) = ⊤

Tactic:
by
    rw [← Finsupp.range_linearCombination]
    exact LinearMap.range_eq_top_of_surjective _ fun x ↦
      ⟨x.coeff, by simp [Finsupp.linearCombination_apply]⟩

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✝ n : ℕ
x✝¹ x✝ : Rep k G
⊢ (functor k G n).map 0 = 0

Tactic:
by simp [map]

Goal state after: