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

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : AddCommMonoid W
inst✝¹ : Module A V
inst✝ : Module A W
ρ : Representation A G V
σ : Representation A G W
e : V ≃ₗ[A] W
he : ∀ (g : G), ↑e ∘ₗ ρ g = σ g ∘ₗ ↑e
g : G
⊢ LinearMap.id ∘ₗ σ g = (σ g ∘ₗ ↑e) ∘ₗ ↑e.symm

Tactic:
id_comp,

Goal state after:
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : AddCommMonoid W
inst✝¹ : Module A V
inst✝ : Module A W
ρ : Representation A G V
σ : Representation A G W
e : V ≃ₗ[A] W
he : ∀ (g : G), ↑e ∘ₗ ρ g = σ g ∘ₗ ↑e
g : G
⊢ σ g = (σ g ∘ₗ ↑e) ∘ₗ ↑e.symm
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
t : ℝ
ht : t < 0
⊢ mgf (-X) μ (-t) ≤ rexp ((↑‖-a - -b‖₊ / 2) ^ 2 * (-t) ^ 2 / 2)

Tactic:
by
      apply ProbabilityTheory.mgf_le_of_mem_Icc_of_integral_eq_zero (hm.neg)
      · filter_upwards [hb] with ω ⟨hl, hr⟩ using ⟨neg_le_neg_iff.2 hr, neg_le_neg_iff.2 hl⟩
      · simp only [Pi.neg_apply]; rw [integral_neg, hc, neg_zero]
      · rwa [Left.neg_pos_iff]

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

Goal state before:
pp: case of
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : k[G]
x : V
g : G
⊢ f ((((lift k (V →ₗ[k] V) G) ρ) ((MonoidAlgebra.of k G) g)) x) =
    (((lift k (W →ₗ[k] W) G) σ) ((MonoidAlgebra.of k G) g)) (f x)

Tactic:
simp only [one_smul, MonoidAlgebra.lift_single, MonoidAlgebra.of_apply]

Goal state after:
case of
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : k[G]
x : V
g : G
⊢ f ((ρ g) x) = (σ g) (f x)
Module: Mathlib.RepresentationTheory.Rep.Iso

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ : ModuleCat k[G]
f : X✝ ⟶ Y✝
g : G
x✝ : RestrictScalars k k[G] ↑X✝
⊢ ({ toAddHom := (ModuleCat.Hom.hom f).toAddHom, map_smul' := ⋯ } ∘ₗ (Representation.ofModule ↑X✝) g) x✝ =
    ((Representation.ofModule ↑Y✝) g ∘ₗ { toAddHom := (ModuleCat.Hom.hom f).toAddHom, map_smul' := ⋯ }) x✝

Tactic:
apply f.hom.map_smul

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
⊢ ρ.invariants.carrier = ⋂ g, Function.fixedPoints ⇑(ρ g)

Tactic:
ext; simp [Function.IsFixedPt]

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: case mp
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
X Y : Rep k G
f : ↑X →ₗ[k] ↑Y
g : G
h : Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹ = f
⊢ Y.ρ g ∘ₗ f ∘ₗ 1 = Y.ρ g ∘ₗ f

Tactic:
Module.End.one_eq_id,

Goal state after:
case mp
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
X Y : Rep k G
f : ↑X →ₗ[k] ↑Y
g : G
h : Y.ρ g ∘ₗ f ∘ₗ X.ρ g⁻¹ = f
⊢ Y.ρ g ∘ₗ f ∘ₗ LinearMap.id = Y.ρ g ∘ₗ f
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: case mpr
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
X Y : Rep k G
f : ↑X →ₗ[k] ↑Y
g : G
h : f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f
⊢ f ∘ₗ 1 = f

Tactic:
Module.End.one_eq_id,

Goal state after:
case mpr
k : Type u
inst✝¹ : CommRing k
G : Type v
inst✝ : Group G
X Y : Rep k G
f : ↑X →ₗ[k] ↑Y
g : G
h : f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f
⊢ f ∘ₗ LinearMap.id = f
Module: Mathlib.RepresentationTheory.Maschke

Goal state before:
pp: k : Type u_1
inst✝⁷ : Field k
G : Type u_2
inst✝⁶ : Finite G
inst✝⁵ : NeZero ↑(Nat.card G)
inst✝⁴ : Group G
V : Type u_3
inst✝³ : AddCommGroup V
inst✝² : Module k[G] V
W : Type u_4
inst✝¹ : AddCommGroup W
inst✝ : Module k[G] W
f : V →ₗ[k[G]] W
hf : f.ker = ⊥
A : Type (max u_1 u_2) := k[G]
this✝² : Module k W := Module.compHom W (algebraMap k A)
this✝¹ : Module k V := Module.compHom V (algebraMap k A)
this✝ : IsScalarTower k A W
this : IsScalarTower k A V
⊢ ∃ g, g ∘ₗ f = LinearMap.id

Tactic:
set φ := (f.restrictScalars k).leftInverse

Goal state after:
k : Type u_1
inst✝⁷ : Field k
G : Type u_2
inst✝⁶ : Finite G
inst✝⁵ : NeZero ↑(Nat.card G)
inst✝⁴ : Group G
V : Type u_3
inst✝³ : AddCommGroup V
inst✝² : Module k[G] V
W : Type u_4
inst✝¹ : AddCommGroup W
inst✝ : Module k[G] W
f : V →ₗ[k[G]] W
hf : f.ker = ⊥
A : Type (max u_1 u_2) := k[G]
this✝² : Module k W := Module.compHom W (algebraMap k A)
this✝¹ : Module k V := Module.compHom V (algebraMap k A)
this✝ : IsScalarTower k A W
this : IsScalarTower k A V
φ : W →ₗ[k] V := (↑k f).leftInverse
⊢ ∃ g, g ∘ₗ f = LinearMap.id
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Semiring k
inst✝ : Monoid G
A : Rep k G
a : ↑A
⊢ (ConcreteCategory.hom (𝟙 A)) a = a

Tactic:
simp [Representation.IntertwiningMap.id]

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
τ : ContRepresentation R G U
φ : ρ.Equiv σ
g : G
⊢ (↑φ.toContinuousLinearEquiv ∘SL ↑φ.symm) ∘SL σ g = (↑φ.toContinuousLinearEquiv ∘SL ρ g) ∘SL ↑φ.symm

Tactic:
simp [φ.isIntertwining g, comp_assoc]

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 G W
φ : H →* G
f : π →ⁱL π'
h : H
x✝ : V
⊢ (f.toContinuousLinearMap ∘SL (π.restrict φ) h) x✝ = ((π'.restrict φ) h ∘SL f.toContinuousLinearMap) x✝

Tactic:
simp [f.toContinuousLinearMap_apply, f.isIntertwining]

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

Goal state before:
pp: case h
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
n : ℕ
a✝ : (fun gv ↦ (ρ gv.1) gv.2 - gv.2) ((fun x ↦ g ^ x) n, α) ∈ ↑(ρ g - LinearMap.id).range
⊢ (ρ g - LinearMap.id) (Fin.partialSum (fun j ↦ (ρ (g ^ ↑j)) α) (Fin.last (n + 1))) =
    (fun gv ↦ (ρ gv.1) gv.2 - gv.2) ((fun x ↦ g ^ x) (n + 1), α)

Tactic:
simpa using ρ.apply_sub_id_partialSum_eq _ _ _

Goal state after:
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:
by
  refine le_antisymm (Submodule.span_le.2 ?_) ?_
  · rintro a ⟨⟨γ, α⟩, rfl⟩
    rcases mem_powers_iff_mem_zpowers.2 (hg γ) with ⟨i, rfl⟩
    induction i with | zero => exact ⟨0, by simp⟩ | succ n _ =>
    use (Fin.partialSum (fun (j : Fin (n + 1)) => ρ (g ^ (j : ℕ)) α) (Fin.last _))
    simpa using ρ.apply_sub_id_partialSum_eq _ _ _
  · rintro x ⟨y, rfl⟩
    simpa using Coinvariants.sub_mem_ker g y

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

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : CommGroup G
inst✝ : Fintype G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
x : ↑(leftRegular k G)
hx : x ∈ (Hom.hom ((leftRegular k G).applyAsHom g - 𝟙 (leftRegular k G))).ker
⊢ (Hom.hom (leftRegular k G).norm).toLinearMap (MonoidAlgebra.single 1 (x.coeff g)) = x

Tactic:
ext γ
    have := coeff_of_leftRegular_of_generator (k := k) g hg x
      (by simpa [sub_hom, sub_eq_zero] using! hx) γ
    simp [norm, Representation.norm, this]

Goal state after:
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u
G✝ : Type v
H✝ : Type v'
inst✝⁴ : CommRing k
inst✝³ : Group G✝
inst✝² : Group H✝
φ✝ : G✝ →* H✝
A✝ : Rep k G✝
G H : Type u
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
A : Rep k G
B : Rep k H
⊢ coinvariantsTensorIndInv φ A B ≫ coinvariantsTensorIndHom φ A B = 𝟙 (((coinvariantsTensor k G).obj A).obj (res φ B))

Tactic:
ext
    simp [coinvariantsTensorIndInv, coinvariantsTensorMk, coinvariantsTensorIndHom]

Goal state after:
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 j : ℕ),
    (ComplexShape.up ℕ).Rel i j →
      A.leftRegularHomEquiv.toModuleIso.hom ≫ (moduleCatCochainComplex A g).d i j =
        ((resolution k g hg).complex.linearYonedaObj k A).d i j ≫ A.leftRegularHomEquiv.toModuleIso.hom

Tactic:
rintro i j ⟨rfl⟩
    ext (x : leftRegular _ _ ⟶ _)
    by_cases hi : Even i
    · have : ¬(Even (i + 1)) := Nat.even_add_one.not_left.mpr hi
      simp [sub_hom, hi, this, homEquiv, ← hom_comm_apply x, Rep.applyAsHom]
    · simp [hi, Nat.even_add_one.2 hi, Representation.norm, homEquiv, Rep.norm, ← hom_comm_apply x]

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
x✝¹ : ↑(ModuleCat.of k ↑A)
x✝ : G
⊢ (ModuleCat.Hom.hom (d₀₁ A)) x✝¹ x✝ = (ModuleCat.Hom.hom 0) x✝¹ x✝

Tactic:
rw [d₀₁_hom_apply, isTrivial_apply, sub_self]

Goal state after:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
x✝¹ : ↑(ModuleCat.of k ↑A)
x✝ : G
⊢ 0 = (ModuleCat.Hom.hom 0) x✝¹ x✝
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (cocyclesIso₀ A).inv ≫ iCocycles A 0 = (shortComplexH0 A).f ≫ (cochainsIso₀ A).inv

Tactic:
rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, cocyclesIso₀_hom_comp_f]

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
M : Rep R G
X✝ : Rep R G
Y✝ : Rep R G
n : ℕ
inst✝ : NeZero n
X Y : Rep R G
f : X ⟶ Y
⊢ (tateCohomologyFunctor ↑n).map f ≫ ((tateComplexConnectData Y).homologyIsoPos n ↑n ⋯).hom =
    ((tateComplexConnectData X).homologyIsoPos n ↑n ⋯).hom ≫ (groupCohomology.functor R G n).map f

Tactic:
simp [tateCohomologyFunctor, CochainComplex.ConnectData.homologyMap_map_of_eq_succ (n := n)]

Goal state after:
Module: Mathlib.RepresentationTheory.Tannaka

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Finite G
η : Aut (forget k G)
f g : G → k
⊢ let α := Hom.hom (η.hom.hom.app rightFDRep).hom;
  α (f * g) = α f * α g

Tactic:
by
  have nat := η.hom.hom.naturality mulRepHom
  have tensor (X Y) : η.hom.hom.app (X ⊗ Y) = (η.hom.hom.app X ⊗ₘ η.hom.hom.app Y) :=
    η.hom.isMonoidal.tensor X Y
  rw [tensor] at nat
  exact ConcreteCategory.congr_hom ((CategoryTheory.forget _).congr_map nat) (f ⊗ₜ[k] g)

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

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ restrictSupportIdeal R (⇑degree ⁻¹' Set.Ici 1) ⋯ ≤ idealOfVars σ R

Tactic:
simp only [SetLike.le_def, restrictSupportIdeal, Submodule.mem_mk, Submodule.mem_toAddSubmonoid,
      ← Submodule.restrictScalars_mem R (idealOfVars σ R)]

Goal state after:
case a
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
⊢ ∀ ⦃x : MvPolynomial σ R⦄,
    x ∈ restrictSupport R (⇑degree ⁻¹' Set.Ici 1) → x ∈ Submodule.restrictScalars R (idealOfVars σ R)
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 = 0
⊢ span (m.leadingTerm '' (B \ {0})) = span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' (B \ {0}))

Tactic:
apply span_leadingTerm_eq_span_monomial

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 = 0
⊢ ∀ p ∈ B \ {0}, IsUnit (m.leadingCoeff p)
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : CommSemiring R
p : MvPowerSeries σ R
x : τ →₀ ℕ
h' : x ∉ Set.range (mapDomain f)
⊢ (coeff x) ((rename f) p) = 0

Tactic:
simp [coeff_rename, Set.Finite.toFinset, Set.preimage_singleton_eq_empty.mpr h']

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hXI : X ∉ I
n : ℕ
F : Fin n → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' : Ideal.map constantCoeff I = span (Set.range (⇑constantCoeff ∘ F))
T : R⟦X⟧ → Fin n → R
hT : ∀ g ∈ I, ∑ i, T g i * constantCoeff (F i) = constantCoeff g
g : R⟦X⟧
hg : g ∈ I
G : ℕ → R⟦X⟧ := fun t ↦ Nat.rec g (fun x G' ↦ mk fun p ↦ (coeff (p + 1)) G' - ∑ i, T G' i * (coeff (p + 1)) (F i)) t
hG : ∀ (n : ℕ), G n ∈ I
hG' : ∀ (n_1 : ℕ), G n_1 - ∑ i, C (T (G n_1) i) * F i = X * G (n_1 + 1)
H : Fin n → R⟦X⟧ := fun i ↦ mk fun n ↦ T (G n) i
h₁ : ∀ (n_1 : ℕ), g - ∑ i, ↑((trunc n_1) (H i)) * F i = X ^ n_1 * G n_1
h₂ : g = ∑ i, H i * F i
⊢ g ∈ Submodule.span R⟦X⟧ (Set.range F)

Tactic:
rw [h₂]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hXI : X ∉ I
n : ℕ
F : Fin n → R⟦X⟧
hJI : Submodule.span R⟦X⟧ (Set.range F) ≤ I
hJ : FG (Submodule.span R⟦X⟧ (Set.range F))
h' : Ideal.map constantCoeff I = span (Set.range (⇑constantCoeff ∘ F))
T : R⟦X⟧ → Fin n → R
hT : ∀ g ∈ I, ∑ i, T g i * constantCoeff (F i) = constantCoeff g
g : R⟦X⟧
hg : g ∈ I
G : ℕ → R⟦X⟧ := fun t ↦ Nat.rec g (fun x G' ↦ mk fun p ↦ (coeff (p + 1)) G' - ∑ i, T G' i * (coeff (p + 1)) (F i)) t
hG : ∀ (n : ℕ), G n ∈ I
hG' : ∀ (n_1 : ℕ), G n_1 - ∑ i, C (T (G n_1) i) * F i = X * G (n_1 + 1)
H : Fin n → R⟦X⟧ := fun i ↦ mk fun n ↦ T (G n) i
h₁ : ∀ (n_1 : ℕ), g - ∑ i, ↑((trunc n_1) (H i)) * F i = X ^ n_1 * G n_1
h₂ : g = ∑ i, H i * F i
⊢ ∑ i, H i * F i ∈ Submodule.span R⟦X⟧ (Set.range F)
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
⊢ Function.Bijective ⇑(IsLocalRing.ResidueField.map (algebraMap R (AdicCompletion (maximalIdeal R) R)))

Tactic:
by
  have := AdicCompletion.isLocalRing_of_fg fg
  refine ⟨RingHom.injective _, fun x ↦ ?_⟩
  rcases residue_surjective x with ⟨y, hy⟩
  rcases Ideal.Quotient.mk_surjective (y.1 1) with ⟨z, hz⟩
  use residue R z
  rw [IsLocalRing.ResidueField.map_residue, ← hy]
  apply (Ideal.Quotient.mk_eq_mk_iff_sub_mem _ _).mpr
  rw [maximalIdeal_eq_map_of_fg fg, ← Submodule.restrictScalars_mem R, ← Ideal.smul_top_eq_map]
  have : (algebraMap R (AdicCompletion (maximalIdeal R) R)) z - y ∈
    (maximalIdeal R) ^ 1 • (⊤ : Submodule R (AdicCompletion (maximalIdeal R) R)) := by
    rw [AdicCompletion.algebraMap_apply, pow_smul_top_eq_ker_eval fg]
    simpa [eval, sub_eq_zero] using hz
  simpa

Goal state after:
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:
rw [coeff_truncTotal _ h, coeff_toAdicCompletionInv, ← MvPolynomial.coeff_sub]

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
⊢ MvPolynomial.coeff x (Quotient.out (↑f (degree x + 1)) - Quotient.out (↑f n)) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_2
τ : Type u_3
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
a : σ → MvPowerSeries τ R
ha : MvPowerSeries.HasSubst a
⊢ MvPowerSeries.subst a (MvPowerSeries.subst (fun x ↦ MvPowerSeries.X i) f) = subst (a i) f

Tactic:
MvPowerSeries.subst_comp_subst_apply
    (HasSubst.const (HasSubst.X _)) ha,

Goal state after:
σ : Type u_2
τ : Type u_3
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
a : σ → MvPowerSeries τ R
ha : MvPowerSeries.HasSubst a
⊢ MvPowerSeries.subst (fun s ↦ MvPowerSeries.subst a (MvPowerSeries.X i)) f = subst (a i) f
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 : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
this : Function.Surjective ⇑(LinearMap.codRestrict (I ^ n • ⊤) ((lsum R) fun i ↦ ↑i • LinearMap.id) ⋯)
x : AdicCompletion I (↥s →₀ M)
⊢ (ofPowSMul I M n) ((map I (LinearMap.codRestrict (I ^ n • ⊤) ((lsum R) fun i ↦ ↑i • LinearMap.id) ⋯)) x) ∈
    (map I ((lsum R) fun i ↦ ↑i • LinearMap.id)).range

Tactic:
exact ⟨x, by rw [← LinearMap.comp_apply, map_comp, LinearMap.subtype_comp_codRestrict]⟩

Goal state after:
Module: Mathlib.RingTheory.Flat.Domain

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : Type u_4
Q : Type u_5
inst✝⁴ : AddCommGroup P
inst✝³ : Module R P
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst✝ : Module.Flat R Q
hf : Injective ⇑f
hg : Injective ⇑g
K : Type u_1 := FractionRing R
H₁ : Injective ⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g))
H₂ : Injective ⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q).symm
H₃ : Injective ⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N)
⊢ Injective (⇑((mk R K (M ⊗[R] N)) 1) ∘ ⇑(map f g))

Tactic:
have H₄ := (AlgebraTensorModule.assoc R R K K P Q).symm.injective

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
P : Type u_4
Q : Type u_5
inst✝⁴ : AddCommGroup P
inst✝³ : Module R P
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
f : P →ₗ[R] M
g : Q →ₗ[R] N
H : Module.Flat R P
inst✝ : Module.Flat R Q
hf : Injective ⇑f
hg : Injective ⇑g
K : Type u_1 := FractionRing R
H₁ : Injective ⇑(map (LinearMap.baseChange K f) (LinearMap.baseChange K g))
H₂ : Injective ⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] P) Q).symm
H₃ : Injective ⇑(AlgebraTensorModule.cancelBaseChange R K K (K ⊗[R] M) N)
H₄ : Injective ⇑(AlgebraTensorModule.assoc R R K K P Q).symm
⊢ Injective (⇑((mk R K (M ⊗[R] N)) 1) ∘ ⇑(map f g))
Module: Mathlib.RingTheory.Coalgebra.Quotient

Goal state before:
pp: case coassoc
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ (↑(TensorProduct.assoc R (C ⧸ I) (C ⧸ I) (C ⧸ I)) ∘ₗ rTensor (C ⧸ I) comul ∘ₗ comul) ∘ₗ I.mkQ =
    (lTensor (C ⧸ I) comul ∘ₗ comul) ∘ₗ I.mkQ

Tactic:
simp only [coassoc_simps, comul_comp_mkQ, counit_comp_mkQ]

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

Goal state before:
pp: case rTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ (rTensor (C ⧸ I) counit ∘ₗ comul) ∘ₗ I.mkQ = (TensorProduct.mk R R (C ⧸ I)) 1 ∘ₗ I.mkQ

Tactic:
simp only [coassoc_simps, comul_comp_mkQ, counit_comp_mkQ]

Goal state after:
case rTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ map counit I.mkQ ∘ₗ comul = (TensorProduct.mk R R (C ⧸ I)) 1 ∘ₗ I.mkQ
Module: Mathlib.RingTheory.Coalgebra.Quotient

Goal state before:
pp: case lTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ (lTensor (C ⧸ I) counit ∘ₗ comul) ∘ₗ I.mkQ = (TensorProduct.mk R (C ⧸ I) R).flip 1 ∘ₗ I.mkQ

Tactic:
simp only [coassoc_simps, comul_comp_mkQ, counit_comp_mkQ]

Goal state after:
case lTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ map I.mkQ counit ∘ₗ comul = (TensorProduct.mk R (C ⧸ I) R).flip 1 ∘ₗ I.mkQ