mathlib-initiative/mathlib-tactics huggingface dataset:
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₃ : G
a : ↑A
⊢ (A.indToCoindAux g₁) a (g₂ * g₃⁻¹) = (A.indToCoindAux (g₁ * g₃)) a g₂

Tactic:
rcases em ((QuotientGroup.rightRel S).r (g₂ * g₃⁻¹) g₁) with ⟨s, hs⟩ | h
  · simp [S.1.smul_def, mul_assoc, ← eq_mul_inv_iff_mul_eq.1 hs]
  · rw [indToCoindAux_of_not_rel (h := h), indToCoindAux_of_not_rel]
    exact mt (fun ⟨s, hs⟩ => ⟨s, by simpa [S.1.smul_def, eq_mul_inv_iff_mul_eq, mul_assoc]⟩) h

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

Goal state before:
pp: 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
f : res (↑φ) X ⟶ Y
i j : ℕ
hij : i + 1 = j
⊢ invariantsResMap (↑φ) (resolutionMap φ f (i + 1)) ≫ Y.homogeneousCochains.d i j =
    X.homogeneousCochains.d i j ≫ invariantsResMap (↑φ) (resolutionMap φ f (j + 1))

Tactic:
subst hij

Goal state after:
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
f : res (↑φ) X ⟶ Y
i : ℕ
⊢ invariantsResMap (↑φ) (resolutionMap φ f (i + 1)) ≫ Y.homogeneousCochains.d i (i + 1) =
    X.homogeneousCochains.d i (i + 1) ≫ invariantsResMap (↑φ) (resolutionMap φ f (i + 1 + 1))
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
x : ↥(Hom.hom A.norm).ker
⊢ (ConcreteCategory.hom (groupCohomologyπOdd A g hg i hi)) x = 0 ↔ ↑x ∈ (Hom.hom (A.applyAsHom g - 𝟙 A)).range

Tactic:
by
  simp [groupCohomologyπOdd, map_eq_zero_iff _ ((ModuleCat.mono_iff_injective _).1 inferInstance),
    moduleCatToCycles, -LinearMap.mem_range, LinearMap.range_codRestrict]

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

Goal state before:
pp: k G✝ : Type u
inst✝² : CommRing k
n✝ : ℕ
inst✝¹ : Monoid G✝
G : Type u
inst✝ : Group G
n : ℕ
⊢ Projective ((standardComplex k G).X n)

Tactic:
by
  exact inferInstanceAs <| Projective (Rep.diagonal k G (n + 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:
subst hij

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
X : ShortComplex (Rep k G)
hX : X.ShortExact
i : ℕ
z : (Fin i → G) → ↑X.X₃
y : (Fin i → G) → ↑X.X₂
hy : (ConcreteCategory.hom ((cochainsMap (MonoidHom.id G) X.g).f i)) y = z
hz : (ConcreteCategory.hom ((inhomogeneousCochains X.X₃).d i (i + 1))) z = 0
x : (Fin (i + 1) → G) → ↑X.X₁
hx : ⇑(Rep.Hom.hom X.f) ∘ x = (ConcreteCategory.hom ((inhomogeneousCochains X.X₂).d i (i + 1))) y
⊢ (ConcreteCategory.hom (inhomogeneousCochains.d X.X₃ i)) z = 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 : ↑(ModuleCat.of k (G → ↑A))
⊢ (ModuleCat.Hom.hom (d₁₂ A)) x ∈ cocycles₂ A

Tactic:
exact d₁₂_apply_mem_cocycles₂ x

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 i j : ℕ
hij : i + 1 = j
⊢ ModuleCat.ofHom ((Hom.hom φ).compLeft (Fin i → G) ∘ₗ LinearMap.funLeft k ↑A fun x ↦ ⇑f ∘ x) ≫
      (inhomogeneousCochains B).d i j =
    (inhomogeneousCochains A).d i j ≫
      ModuleCat.ofHom ((Hom.hom φ).compLeft (Fin j → G) ∘ₗ LinearMap.funLeft k ↑A fun x ↦ ⇑f ∘ x)

Tactic:
subst hij

Goal state after:
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 i : ℕ
⊢ ModuleCat.ofHom ((Hom.hom φ).compLeft (Fin i → G) ∘ₗ LinearMap.funLeft k ↑A fun x ↦ ⇑f ∘ x) ≫
      (inhomogeneousCochains B).d i (i + 1) =
    (inhomogeneousCochains A).d i (i + 1) ≫
      ModuleCat.ofHom ((Hom.hom φ).compLeft (Fin (i + 1) → G) ∘ₗ LinearMap.funLeft k ↑A fun x ↦ ⇑f ∘ x)
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R⟦X⟧
inst✝ : I.IsPrime
hI : X ∉ I
S : Set R
hSI : span S = Ideal.map constantCoeff I
hS : S.Finite
this : SurjOn (⇑constantCoeff) (↑I) S
T : Set R⟦X⟧
hTI : T ⊆ ↑I
hinj : InjOn (⇑constantCoeff) T
hT : ⇑constantCoeff '' T = S
f✝ : R⟦X⟧
hf✝ : constantCoeff f✝ ∈ span S
r₁ r₂ : R
hr₁ : r₂ ∈ Submodule.span R S
f : R⟦X⟧
hfmem : f ∈ span T
hf : constantCoeff f = r₂
⊢ constantCoeff (r₁ • f) = r₁ • r₂

Tactic:
by simp [hf]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
n : ℕ
S : Type u_3
inst✝² : CommRing S
inst✝¹ : IsNoetherianRing S
inst✝ : Finite σ
⊢ IsNoetherianRing (MvPowerSeries σ S)

Tactic:
cases nonempty_fintype σ
  have := isNoetherianRing_fin S (Fintype.card σ)
  exact isNoetherianRing_of_ringEquiv (MvPowerSeries (Fin (Fintype.card σ)) S)
    (renameEquiv S (Fintype.equivFin σ)).toRingEquiv.symm

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 i j : ℕ
hij : j + 1 = i
⊢ ModuleCat.ofHom (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ lmapDomain (↑A) k fun x ↦ ⇑f ∘ x) ≫
      (inhomogeneousChains B).d i j =
    (inhomogeneousChains A).d i j ≫
      ModuleCat.ofHom (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ lmapDomain (↑A) k fun x ↦ ⇑f ∘ x)

Tactic:
subst hij

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 j : ℕ
⊢ ModuleCat.ofHom (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ lmapDomain (↑A) k fun x ↦ ⇑f ∘ x) ≫
      (inhomogeneousChains B).d (j + 1) j =
    (inhomogeneousChains A).d (j + 1) j ≫
      ModuleCat.ofHom (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ lmapDomain (↑A) k fun x ↦ ⇑f ∘ x)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

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

Tactic:
by simp [coeff_truncTotal _ hx]

Goal state after:
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
hx : ∀ {m n : ℕ}, m ≤ n → x m ≡ x n [SMOD I ^ m • ⊤]
⊢ ∃ L, ∀ (n : ℕ), x n ≡ L [SMOD I ^ n • ⊤]

Tactic:
let L : AdicCompletion I M := {
      val i := (x i).val i
      property {m n} h' := by
        simp only [transitionMap_comp_eval_apply]
        specialize hx h'
        rwa [SModEq.sub_mem, pow_smul_top_eq_ker_eval h, LinearMap.mem_ker, _root_.map_sub,
          sub_eq_zero, eval_apply, eval_apply, eq_comm] at hx
    }

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
hx : ∀ {m n : ℕ}, m ≤ n → x m ≡ x n [SMOD I ^ m • ⊤]
L : AdicCompletion I M := ⟨fun i ↦ ↑(x i) i, ⋯⟩
⊢ ∃ L, ∀ (n : ℕ), x n ≡ L [SMOD I ^ n • ⊤]
Module: Mathlib.RingTheory.Bialgebra.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ Bialgebra R (A ⧸ I)

Tactic:
by
  refine .ofAlgHom (comulAlgHom I) (counitAlgHom I) ?_ ?_ ?_ <;>
    refine Ideal.Quotient.algHom_ext R (AlgHom.toLinearMap_injective ?_) <;>
    simp only [coassoc_simps, AlgHom.comp_toLinearMap, Algebra.TensorProduct.toLinearMap_map,
      comul_comp_mkₐ, counit_comp_mkₐ]
  · simp [coassoc_simps]
  · rw [CoassocSimps.map_counit_comp_comul_left]; rfl
  · rw [CoassocSimps.map_counit_comp_comul_right]; rfl

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: case mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ fromUnit.ker
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  (powMonoidHom n) { val := v, inv := i, val_inv := vi, inv_val := iv } =
    (Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑{ val := v, inv := i, val_inv := vi, inv_val := iv } ^ n =
    (algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑({ val := v, inv := i, val_inv := vi, inv_val := iv } ^ n)⁻¹ =
    (algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ (powMonoidHom n).range

Tactic:
← inv_pow,

Goal state after:
case mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
hx✝ : { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ fromUnit.ker
v i : K
vi : v * i = 1
iv : i * v = 1
hx :
  (powMonoidHom n) { val := v, inv := i, val_inv := vi, inv_val := iv } =
    (Units.map ↑(algebraMap R K)) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hv :
  ↑{ val := v, inv := i, val_inv := vi, inv_val := iv } ^ n =
    (algebraMap R K) ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
hi :
  ↑({ val := v, inv := i, val_inv := vi, inv_val := iv }⁻¹ ^ n) =
    (algebraMap R K) { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ (powMonoidHom n).range
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: case h
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Ideal.span ↑T = Ideal.comap (algebraMap R R') p
m : M
s : ↥S
hx : p = (⊥.colon {IsLocalizedModule.mk' f m s}).radical
e : ↥T → ℕ
g : ↥T → ↥S
hg : ∀ (a : ↥T), g a • ↑a ^ e a • m = 0
a : R
ha : a ∈ ↑T
u : ↥S
hu : ∏ a, g a = g ⟨a, ha⟩ * u
⊢ a ^ e ⟨a, ha⟩ • (↑(g ⟨a, ha⟩) * ↑u) • m = 0

Tactic:
smul_smul,

Goal state after:
case h
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Ideal.span ↑T = Ideal.comap (algebraMap R R') p
m : M
s : ↥S
hx : p = (⊥.colon {IsLocalizedModule.mk' f m s}).radical
e : ↥T → ℕ
g : ↥T → ↥S
hg : ∀ (a : ↥T), g a • ↑a ^ e a • m = 0
a : R
ha : a ∈ ↑T
u : ↥S
hu : ∏ a, g a = g ⟨a, ha⟩ * u
⊢ (a ^ e ⟨a, ha⟩ * (↑(g ⟨a, ha⟩) * ↑u)) • m = 0
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
n✝ : ℕ
x✝¹ : A
x✝ : x✝¹ ∈ I
⊢ hI.dpow n✝ ((RingHom.id A) x✝¹) = (RingHom.id A) (hI.dpow n✝ x✝¹)

Tactic:
by simp only [RingHom.id_apply]

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = span S
hS' : ∀ s ∈ S, f s ∈ J
hdp : ∀ {n : ℕ}, ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)
a : A
has : a ∈ S
⊢ f a ∈ ↑J

Tactic:
exact hS' a has

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case insert
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec : s.Nonempty → (∀ i ∈ s, r i ∈ I) → hI.dpow n (∏ i ∈ s, r i) = n ! ^ (#s - 1) • ∏ i ∈ s, hI.dpow n (r i)
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
⊢ hI.dpow n (∏ i ∈ insert a s, r i) = n ! ^ (#(insert a s) - 1) • ∏ i ∈ insert a s, hI.dpow n (r i)

Tactic:
| @insert a s has hrec =>

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
hhI : ∀ {n : ℕ}, n ≠ 0 → ∀ s ∈ S, hI.dpow n s ∈ span S
hSI : span S ≤ I
z x y : A
hxI : x ∈ Submodule.span A S
hyI : y ∈ Submodule.span A S
hx : ∀ (m : ℕ), m ≠ 0 → hI.dpow m x ∈ span S
hy : ∀ (m : ℕ), m ≠ 0 → hI.dpow m y ∈ span S
m✝ : ℕ
hm : m✝ ≠ 0
m : ℕ
a✝ : m ∈ range (m✝ + 1)
hm0 : m = 0
⊢ hI.dpow m x * hI.dpow (m✝ - m) y ∈ span S

Tactic:
exact hm0 ▸ mul_mem_left (span S) _ (hy _ hm)

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case inr.inl
K : Type u_2
inst✝ : DivisionRing K
a : K[ε]
ha : IsNilpotent a
b : K[ε]ˣ
⊢ ∃ c, a * c = ↑b ∨ ↑b * c = a

Tactic:
exact ⟨b⁻¹ * a, by simp⟩

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring

Goal state before:
pp: case mem
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
s : Set A
h : ∀ (i : ι) ⦃x : A⦄, x ∈ s → ↑(((decompose 𝒜) x) i) ∈ s
x x✝ : A
hx : x✝ ∈ s
i : ι
⊢ ↑(((decompose 𝒜) x✝) i) ∈ Subsemiring.closure s

Tactic:
| mem _ hx =>

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring

Goal state before:
pp: case inr
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
x : A
hx✝ : x ∈ insert 0 s
hx : x ∈ s
j : ι
hj : x ∈ 𝒜 j
⊢ ↑(((decompose 𝒜) x) i) ∈ insert 0 s

Tactic:
obtain rfl | h := eq_or_ne i j <;> simp [decompose_of_mem _ hj, of_eq_of_ne, *]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r s : R
⊢ binomialSeries A (r + s) = binomialSeries A r * binomialSeries A s

Tactic:
ext n
  simp only [binomialSeries_coeff, Ring.add_choose_eq n (Commute.all r s), coeff_mul,
    Algebra.mul_smul_comm, mul_one, sum_smul]
  refine sum_congr rfl fun ab hab => ?_
  rw [mul_comm, mul_smul]

Goal state after:
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
σ✝ : Type u_3
τ : Type u_4
σ : Type u_5
F : FormalGroup R
⊢ 𝔾ₐ.toPowerSeries = subst ![X₁, X₀] 𝔾ₐ.toPowerSeries

Tactic:
by simp [subst_add .X_X, subst_X .X_X, add_comm]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case h
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
c : ℕ × ℕ
hcn : c.1 + c.2 = n
hc : (PowerSeries.coeff c.1) a • (PowerSeries.coeff c.2) b • (x ^ n).coeff g ≠ 0
⊢ ((PowerSeries.coeff c.1) a • (PowerSeries.coeff c.2) b • x ^ n).coeff g ≠ 0

Tactic:
simp [hc]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
h : ¬0 < x.orderTop
⊢ (PowerSeries.constantCoeff a * PowerSeries.constantCoeff b) • 1 =
    PowerSeries.constantCoeff a • 1 * PowerSeries.constantCoeff b • 1

Tactic:
rw [smul_mul_smul_comm, mul_one]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
u : R⟦X⟧ˣ
⊢ ∃ b, (heval x) ↑u * b = 1

Tactic:
use heval x u.inv

Goal state after:
case h
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
u : R⟦X⟧ˣ
⊢ (heval x) ↑u * (heval x) u.inv = 1
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : α → R⟦Γ⟧
t : β → V⟦Γ'⟧
hs : (⋃ a, (s a).support).IsPWO
ht : (⋃ b, (t b).support).IsPWO
hsupp :
  ∀ (ab : α × β), ((fun ab ↦ (of R).symm (s ab.1 • (of R) (t ab.2))) ab).support ⊆ (s ab.1).support +ᵥ (t ab.2).support
⊢ ⋃ a, ((fun a ↦ (of R).symm (s a.1 • (of R) (t a.2))) a).support ⊆ (⋃ a, (s a).support) +ᵥ ⋃ b, (t b).support

Tactic:
refine Set.Subset.trans (Set.iUnion_mono fun a => (hsupp a)) ?_

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddCommMonoid V
inst✝³ : AddCommMonoid R
inst✝² : SMulWithZero R V
inst✝¹ : VAdd Γ Γ'
inst✝ : IsOrderedCancelVAdd Γ Γ'
s : α → R⟦Γ⟧
t : β → V⟦Γ'⟧
hs : (⋃ a, (s a).support).IsPWO
ht : (⋃ b, (t b).support).IsPWO
hsupp :
  ∀ (ab : α × β), ((fun ab ↦ (of R).symm (s ab.1 • (of R) (t ab.2))) ab).support ⊆ (s ab.1).support +ᵥ (t ab.2).support
⊢ ⋃ i, (s i.1).support +ᵥ (t i.2).support ⊆ (⋃ a, (s a).support) +ᵥ ⋃ b, (t b).support
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ ![f, 0] ((fun i ↦ i) ⟨0, ⋯⟩) = subst (fun x ↦ f) (![PowerSeries.X, 0] ((fun i ↦ i) ⟨0, ⋯⟩))

Tactic:
simp [PowerSeries.X, subst]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case pos
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
gh : Γ × Γ'
x✝ : gh ∈ VAddAntidiagonal g ⋯
hgh : ¬s.hsum.coeff gh.1 = 0 → ¬t.hsum.coeff gh.2 = 0 → ¬gh.1 +ᵥ gh.2 = g
h : s.hsum.coeff gh.1 = 0
⊢ s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0

pp: case neg
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
gh : Γ × Γ'
x✝ : gh ∈ VAddAntidiagonal g ⋯
hgh : ¬s.hsum.coeff gh.1 = 0 → ¬t.hsum.coeff gh.2 = 0 → ¬gh.1 +ᵥ gh.2 = g
h : ¬s.hsum.coeff gh.1 = 0
⊢ s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0

Tactic:
· exact smul_eq_zero_of_left h (t.hsum.coeff gh.2)

Goal state after:
case neg
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
gh : Γ × Γ'
x✝ : gh ∈ VAddAntidiagonal g ⋯
hgh : ¬s.hsum.coeff gh.1 = 0 → ¬t.hsum.coeff gh.2 = 0 → ¬gh.1 +ᵥ gh.2 = g
h : ¬s.hsum.coeff gh.1 = 0
⊢ s.hsum.coeff gh.1 • t.hsum.coeff gh.2 = 0
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case «1»
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f : MvPowerSeries σ R
hf : PowerSeries.HasSubst f
⊢ ![0, f] ((fun i ↦ i) ⟨1, ⋯⟩) = subst (fun x ↦ f) (![0, PowerSeries.X] ((fun i ↦ i) ⟨1, ⋯⟩))

Tactic:
simp [PowerSeries.X, subst]

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
α : Type u_5
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
R : Type u_7
inst✝ : Ring R
s t : SummableFamily Γ R α
⊢ lsum s - lsum t = s.hsum - t.hsum

Tactic:
lsum_apply,

Goal state after:
Γ : Type u_1
α : Type u_5
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
R : Type u_7
inst✝ : Ring R
s t : SummableFamily Γ R α
⊢ s.hsum - lsum t = s.hsum - t.hsum
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
⊢ (1 • powers x - x • powers x).hsum = 1

Tactic:
one_smul,

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : 0 < x.orderTop
⊢ (powers x - x • powers x).hsum = 1