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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ rexp (↑cX * t ^ 2 / 2) * rexp (↑cY * t ^ 2 / 2) = rexp ((↑cX + ↑cY) * t ^ 2 / 2)

Tactic:
← exp_add

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ rexp (↑cX * t ^ 2 / 2 + ↑cY * t ^ 2 / 2) = rexp ((↑cX + ↑cY) * t ^ 2 / 2)
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
ε : ℝ
ε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 : ℕ
⊢ ∑ j ∈ range (u (N - 1)), c ^ 5 * (c - 1)⁻¹ ^ 3 / ↑j ^ 2 * Var[Y j; ℙ] =
    c ^ 5 * (c - 1)⁻¹ ^ 3 * ∑ j ∈ range (u (N - 1)), (↑j ^ 2)⁻¹ * Var[Y j; ℙ]

Tactic:
simp_rw [mul_sum, div_eq_mul_inv, mul_assoc]

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
⊢ ∀ (x : ρ.IntertwiningMap ρ) (n : ℕ), (x ^ n).toLinearMap = x.toLinearMap ^ n

Tactic:
by
      intro f n
      induction n with
      | zero => rfl
      | succ n ih => simp [ih, pow_succ]

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

Goal state before:
pp: k : Type u
inst✝² : Semiring k
G : Type v1
H : Type v2
inst✝¹ : Monoid G
inst✝ : Monoid H
f : H →* G
M : Rep k G
X Y : Rep k G
hf : Function.Surjective ⇑f
f' : res f X ⟶ res f Y
g : G
⊢ (Hom.hom f').toLinearMap ∘ₗ X.ρ g = Y.ρ g ∘ₗ (Hom.hom f').toLinearMap

Tactic:
obtain ⟨h, rfl⟩ := hf g; simpa using f'.hom.2 h

Goal state after:
Module: Mathlib.RepresentationTheory.Irreducible

Goal state before:
pp: G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst✝⁷ : Monoid G
inst✝⁶ : Field k
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
inst✝³ : AddCommGroup W
inst✝² : Module k W
ρ : Representation k G V
σ : Representation k G W
f : ρ.IntertwiningMap σ
inst✝¹ : ρ.IsIrreducible
inst✝ : σ.IsIrreducible
⊢ Bijective ⇑f ∨ f = 0

Tactic:
rw [← LinearEquiv.map_eq_zero_iff (equivLinearMapAsModule ρ σ)]
  exact LinearMap.bijective_or_eq_zero (equivLinearMapAsModule ρ σ f)

Goal state after:
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: G : Type u_1
k : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : Monoid G
inst✝⁴ : Field k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
ρ : Representation k G V
σ : Representation k G W
φ : ρ.Equiv σ
⊢ ρ.character = σ.character

Tactic:
by
  ext g
  simp [character, ← φ.conj_apply_self]

Goal state after:
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
| (↑(Nat.card G))⁻¹ * ∑ g, W.character g * V.character g⁻¹

Tactic:
congr; rfl; congr; rfl; intro _; rw [mul_comm, ← FDRep.char_linHom]

Goal state after:
case a.f
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
x✝ : G
| (of (linHom V.ρ W.ρ)).character x✝
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: case refine_1
k : Type u
G✝ : Type v
H : Type w
inst✝⁴ : CommRing k
inst✝³ : Monoid G✝
inst✝² : Monoid H
φ : G✝ →* H
A : Rep k G✝
G : Type v'
inst✝¹ : Group G
S : Subgroup G
X Y : Rep k ↥S
f : X ⟶ Y
inst✝ : Epi f
y : ↑((coindFunctor k S.subtype).obj Y)
this : Setoid G := QuotientGroup.rightRel S
s : ↑Y → ↑X
hs : ∀ (b : ↑Y), (Hom.hom f) (s b) = b
i : Quotient this → G
hi : ∀ (b : Quotient this), Quotient.mk' (i b) = b
γ : G → ↥S := fun g ↦ ⟨g * (i (Quotient.mk' g))⁻¹, ⋯⟩
hmk : ∀ (s : ↥S) (g : G), Quotient.mk' (↑s * g) = Quotient.mk' g
hγ : ∀ (s : ↥S) (g : G), γ (↑s * g) = s * γ g
x : G → ↑X := fun g ↦ (X.ρ (γ g)) (s (↑y (i (Quotient.mk' g))))
x✝¹ : ↥S
x✝ : G
⊢ x (S.subtype x✝¹ * x✝) = (X.ρ x✝¹) (x x✝)

Tactic:
simp [x, ← Module.End.mul_apply, ← map_mul, hmk, hγ]

Goal state after:
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
⊢ resolutionMap (φ.comp ψ) ((resFunctor ↑ψ).map f ≫ g) (i + 1) =
    (resFunctor ↑ψ).map (resolutionMap φ f (i + 1)) ≫ resolutionMap ψ g (i + 1)

Tactic:
rw [resolutionMap_succ, resolutionMap_succ, resolutionMap_succ, 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.FiniteCyclic

Goal state before:
pp: 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
⊢ Coinvariants.ker ρ = (ρ g - LinearMap.id).range

Tactic:
refine le_antisymm (Submodule.span_le.2 ?_) ?_

Goal state after:
case refine_1
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
⊢ (Set.range fun gv ↦ (ρ gv.1) gv.2 - gv.2) ⊆ ↑(ρ g - LinearMap.id).range

case refine_2
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
⊢ (ρ g - LinearMap.id).range ≤ Coinvariants.ker ρ
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
⊢ A.coindToInd ∘ₗ A.indToCoind = LinearMap.id

Tactic:
ext g a
  simp only [LinearMap.comp_apply, AlgebraTensorModule.curry_apply,
    TensorProduct.curry_apply, LinearMap.coe_restrictScalars, LinearMap.id_apply]
  rw [coindToInd_of_support_subset_orbit g]
  · simp
  · intro x hx
    contrapose hx
    simpa using indToCoindAux_of_not_rel g x a hx

Goal state after:
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:
rw [LinearMap.mem_ker, Subtype.ext_iff, ContinuousLinearMap.coe_coe,
    homogeneousCochains.d_apply]
  simp [d_succ, hom_sub, ContIntertwiningMap.sub_apply, d_zero]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Monoid G
A : Rep k G
n : ℕ
f g : (Fin n → G) → ↑A
x✝ : Fin (n + 1) → G
⊢ (A.ρ (x✝ 0)) ((f + g) fun i ↦ x✝ i.succ) + ∑ j, (-1) ^ (↑j + 1) • (f + g) (j.contractNth (fun x1 x2 ↦ x1 * x2) x✝) =
    ((fun g ↦ (A.ρ (g 0)) (f fun i ↦ g i.succ) + ∑ j, (-1) ^ (↑j + 1) • f (j.contractNth (fun x1 x2 ↦ x1 * x2) g)) +
        fun g_1 ↦
        (A.ρ (g_1 0)) (g fun i ↦ g_1 i.succ) + ∑ j, (-1) ^ (↑j + 1) • g (j.contractNth (fun x1 x2 ↦ x1 * x2) g_1))
      x✝

Tactic:
simp [Finset.sum_add_distrib, add_add_add_comm]

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
⊢ (cochainsMap f φ).f 0 ≫ (cochainsIso₀ B).hom = (cochainsIso₀ A).hom ≫ Hom.toModuleCatHom φ

Tactic:
by
  ext x
  simp only [cochainsMap_f, Unique.eq_default (f ∘ _)]
  rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
⊢ { toFun := fun f t ↦ f (t * 1), map_add' := ⋯, map_smul' := ⋯ } = 1

Tactic:
ext
    simp

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
⊢ { toFun := fun f t ↦ f (1⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ } = 1

Tactic:
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 : ℕ
x : ↑(shortComplexH2 A).X₁
g : G × G
⊢ (ModuleCat.Hom.hom (cochainsMap₁ f φ ≫ (shortComplexH2 B).f)) x g =
    (ModuleCat.Hom.hom ((shortComplexH2 A).f ≫ cochainsMap₂ f φ)) x g

Tactic:
simp [shortComplexH2, ← hom_comm_apply φ]

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 : ℕ
x : ↑(shortComplexH2 A).X₂
g : G × G × G
⊢ (ModuleCat.Hom.hom (cochainsMap₂ f φ ≫ (shortComplexH2 B).g)) x g =
    (ModuleCat.Hom.hom ((shortComplexH2 A).g ≫ cochainsMap₃ f φ)) x g

Tactic:
simp [shortComplexH2, ← hom_comm_apply φ]

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
⊢ { toRingHom := eval₂Hom (algebraMap A (MvPolynomial σ A ⧸ I)) fun d ↦ (Ideal.Quotient.mk I) (X d), commutes' := ⋯ }
      d =
    eval₂ (algebraMap A (MvPolynomial σ A ⧸ I)) (fun d ↦ (Ideal.Quotient.mk I) (X d)) d

Tactic:
AlgHom.coe_mk,

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
hp : p ∈ B
⊢ (MvPolynomial.monomial (m.degree p)) 1 = MvPolynomial.C ↑⋯.unit⁻¹ * m.leadingTerm p

Tactic:
← C_mul_leadingCoeff_monomial_degree,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
hB : ∀ p ∈ B, IsUnit (m.leadingCoeff p)
p : MvPolynomial σ R
hp : p ∈ B
⊢ (MvPolynomial.monomial (m.degree p)) 1 =
    MvPolynomial.C ↑⋯.unit⁻¹ * (MvPolynomial.C (m.leadingCoeff p) * (MvPolynomial.monomial (m.degree p)) 1)
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : Semiring R
x : σ →₀ ℕ
r : R
⊢ renameFun f ((monomial x) r) = (monomial (mapDomain f x)) r

Tactic:
classical
  ext; simp [coeff_renameFun, coeff_monomial, eq_comm]

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 × G
a : ↑A
⊢ (ConcreteCategory.hom (d₂₁ A)) (single g a) = single g.2 ((A.ρ g.1⁻¹) a) - single (g.1 * g.2) a + single g.1 a

Tactic:
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 (1, g) a) = single 1 a

Tactic:
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, 1) a) = single 1 ((A.ρ g⁻¹) a)

Tactic:
simp [d₂₁]

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

Goal state before:
pp: case h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
a : ↑A
⊢ (ModuleCat.Hom.hom (d₂₁ A)) (single (1, 1) a) = single 1 a

Tactic:
simp [d₂₁]

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen[inst✝¹] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
n : ℕ
hn : 0 < n
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
⊢ ↑((J ^ n) ^ m) ⊆ ↑(J ^ m)

Tactic:
cases n

Goal state after:
case h.zero
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen[inst✝¹] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
hn : 0 < 0
⊢ ↑((J ^ 0) ^ m) ⊆ ↑(J ^ m)

case h.succ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
h : (∀ (n : ℕ), IsOpen[inst✝¹] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
n✝ : ℕ
hn : 0 < n✝ + 1
⊢ ↑((J ^ (n✝ + 1)) ^ m) ⊆ ↑(J ^ m)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x✝ : MvPowerSeries (Option σ) R
n✝ : Option σ →₀ ℕ
⊢ (coeff n✝) (optionInvFunLeft σ R (optionFunLeft σ R x✝)) = (coeff n✝) x✝

Tactic:
simp [coeff_optionInvFunLeft, coeff_coeff_optionFunLeft]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x✝ : PowerSeries (MvPowerSeries σ R)
n✝¹ : ℕ
n✝ : σ →₀ ℕ
⊢ (coeff n✝) ((PowerSeries.coeff n✝¹) (optionFunLeft σ R (optionInvFunLeft σ R x✝))) =
    (coeff n✝) ((PowerSeries.coeff n✝¹) x✝)

Tactic:
simp [coeff_optionInvFunLeft, coeff_coeff_optionFunLeft]

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

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
this : IsLocalRing (AdicCompletion (maximalIdeal R) R)
x : IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R)
y : AdicCompletion (maximalIdeal R) R
hy : (residue (AdicCompletion (maximalIdeal R) R)) y = x
z : R
hz : (Ideal.Quotient.mk (maximalIdeal R ^ 1 • ⊤)) z = ↑y 1
⊢ (IsLocalRing.ResidueField.map (algebraMap R (AdicCompletion (maximalIdeal R) R))) ((residue R) z) = x

Tactic:
rw [IsLocalRing.ResidueField.map_residue, ← hy]

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
this : IsLocalRing (AdicCompletion (maximalIdeal R) R)
x : IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R)
y : AdicCompletion (maximalIdeal R) R
hy : (residue (AdicCompletion (maximalIdeal R) R)) y = x
z : R
hz : (Ideal.Quotient.mk (maximalIdeal R ^ 1 • ⊤)) z = ↑y 1
⊢ (residue (AdicCompletion (maximalIdeal R) R)) ((algebraMap R (AdicCompletion (maximalIdeal R) R)) z) =
    (residue (AdicCompletion (maximalIdeal R) R)) y
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
comapeq :
  comap (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal (AdicCompletion (maximalIdeal R) R)) =
    maximalIdeal R
f : (maximalIdeal R).Cotangent →ₗ[R] (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent :=
  (maximalIdeal R).mapCotangent (maximalIdeal (AdicCompletion (maximalIdeal R) R))
    (Algebra.ofId R (AdicCompletion (maximalIdeal R) R)) ⋯
⊢ Function.Injective ⇑f

Tactic:
← LinearMap.ker_eq_bot,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
comapeq :
  comap (algebraMap R (AdicCompletion (maximalIdeal R) R)) (maximalIdeal (AdicCompletion (maximalIdeal R) R)) =
    maximalIdeal R
f : (maximalIdeal R).Cotangent →ₗ[R] (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent :=
  (maximalIdeal R).mapCotangent (maximalIdeal (AdicCompletion (maximalIdeal R) R))
    (Algebra.ofId R (AdicCompletion (maximalIdeal R) R)) ⋯
⊢ f.ker = ⊥
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ✝ : Type u_1
R✝ : Type u_2
n✝ : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
n : ℕ
p : MvPolynomial σ R
x : σ →₀ ℕ
h : degree x < n
⊢ MvPolynomial.coeff x ((truncTotal n) ↑p) = MvPolynomial.coeff x p

Tactic:
coeff_truncTotal _ h,

Goal state after:
σ✝ : Type u_1
R✝ : Type u_2
n✝ : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
n : ℕ
p : MvPolynomial σ R
x : σ →₀ ℕ
h : degree x < n
⊢ (coeff x) ↑p = MvPolynomial.coeff x p
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ MvPolynomial.coeff x ((truncTotal n) (toAdicCompletionInv σ R f)) - MvPolynomial.coeff x (Quotient.out (↑f n)) = 0

Tactic:
coeff_truncTotal _ h,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
x : σ →₀ ℕ
h : degree x < n
⊢ (coeff x) (toAdicCompletionInv σ R f) - MvPolynomial.coeff x (Quotient.out (↑f n)) = 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
n : ℕ
⊢ Function.Injective ⇑(ofPowSMul I M n)

Tactic:
← LinearMap.ker_eq_bot,

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
⊢ (ofPowSMul I M n).ker = ⊥
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
⊢ ↑(s x) = y

Tactic:
← hs y,

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) = ↑(s y)
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
⊢ LinearIndepOn R id {a | IsGroupLikeElem R a}

Tactic:
by
  classical
  -- We show that any finset `s` of group-like elements is linearly independent.
  rw [linearIndepOn_iff_linearIndepOn_finset]
  rintro s hs
  -- For this, we do induction on `s`.
  induction s using Finset.cons_induction with
  -- The case `s = ∅` is trivial.
  | empty => simp
  -- Let's deal with the `s ∪ {a}` case.
  | cons a s has ih =>
  simp only [Finset.cons_eq_insert, Finset.coe_insert, Set.subset_def, Set.mem_insert_iff,
    Finset.mem_coe, Set.mem_ofPred_eq, forall_eq_or_imp] at hs
  obtain ⟨ha, hs⟩ := hs
  specialize ih hs
  -- Assume that there is some `c : A → R` and `d : R` such that `∑ x ∈ s, c x • x = d • a`.
  -- We want to prove `d = 0` and `∀ x ∈ s, c x = 0`.
  rw [Finset.coe_cons]
  refine ih.id_insert' ?_
  simp only [mem_span_finset, forall_exists_index, and_imp]
  rintro d c - hc
  -- `x ⊗ y` over `x, y ∈ s` are linearly independent since `s` is linearly independent and
  -- `R` is a domain.
  replace ih := ih.tmul_of_isDomain ih
  simp_rw [← Finset.coe_product, linearIndepOn_finset_iffₛ, id] at ih
  -- Tensoring the equality `∑ x ∈ s, c x • x = d • a` with itself, we get by linear independence
  -- that `c x ^ 2 = d * c x` and `c x * c y = 0` for `x ≠ y`.
  have key := calc
        ∑ x ∈ s, ∑ y ∈ s, (if x = y then d * c x else 0) • x ⊗ₜ[R] y
    _ = d • ∑ x ∈ s, c x • x ⊗ₜ[R] x := by simp [Finset.smul_sum, mul_smul]
    _ = d • comul (d • a) := by rw [← hc]; simp +contextual [(hs _ _).comul_eq_tmul_self]
    _ = (d • a) ⊗ₜ (d • a) := by simp [ha.comul_eq_tmul_self, smul_tmul, tmul_smul, -neg_smul]
    _ = ∑ x ∈ s, ∑ y ∈ s, (c x * c y) • x ⊗ₜ[R] y := by
      simp_rw [← hc, sum_tmul, smul_tmul, Finset.smul_sum, tmul_sum, tmul_smul, mul_smul]
  simp_rw [← Finset.sum_product'] at key
  apply ih at key
  -- Therefore, `c x = 0` for all `x ∈ s`.
  replace key x (hx : x ∈ s) : c x = 0 := by
    -- Otherwise, we deduce from `key` that `c y = 0` for any `y ≠ x` with `y ∈ s`.
    by_contra! hcx
    have hcy (y) (hys : y ∈ s) (hyx : y ≠ x) : c y = 0 := by
      simpa [*] using (key (y, x) (by simp [*])).symm
    -- Then substitute this into `hc` to get `c x • x = d • a`.
    rw [Finset.sum_eq_single x (by simp +contextual [hcy]) (by simp [hx])] at hc
    -- But `key` also says that `c x = d`.
    have hcxa : d = c x := mul_left_injective₀ hcx (by simpa using (key (x, x) (by simp [*])))
    -- So `x = a`...
    obtain rfl : x = a := by rwa [hcxa, smul_right_inj hcx] at hc
    -- ... which contradicts `x ∈ s` and `a ∉ s`.
    contradiction
  -- We are now done, since `d • a = ∑ x ∈ s, c x • x = 0`
  simp_all [ha.ne_zero, eq_comm]

Goal state after: