mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90

Goal state before:
pp: K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
⊢ Module.IsTorsionFree A L

Tactic:
Module.isTorsionFree_iff_algebraMap_injective,

Goal state after:
K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
⊢ Function.Injective ⇑(algebraMap A L)
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 : ℕ
this : (Rep.Hom.hom X.f).range = (Rep.Hom.hom X.g).ker
⊢ ((X.map (cochainsFunctor k G)).map (HomologicalComplex.eval (ModuleCat k) (ComplexShape.up ℕ) i)).Exact

Tactic:
simp [moduleCat_exact_iff_range_eq_ker, LinearMap.range_compLeft,
        LinearMap.ker_compLeft, this]

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
f : ↥(cocycles₂ A)
g : G
⊢ f (g, 1) = (A.ρ g) (f (1, 1))

Tactic:
have := (mem_cocycles₂_iff f).1 f.2 g 1 1

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : ↥(cocycles₂ A)
g : G
this : f (g * 1, 1) + f (g, 1) = (A.ρ g) (f (1, 1)) + f (g, 1 * 1)
⊢ f (g, 1) = (A.ρ g) (f (1, 1))
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

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

Tactic:
by
  simp [isoCocycles₁, iCocycles, HomologicalComplex.iCycles, iCycles]

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
hg : ∀ (x : G), x ∈ Subgroup.zpowers g✝
j : ℕ
a : ↑A
g : G
⊢ (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X (j + 1))).compr₂
            (ModuleCat.Hom.hom
              (A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom ≫ (moduleCatChainComplex A g✝).d (j + 1) j)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1 =
    (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X (j + 1))).compr₂
            (ModuleCat.Hom.hom
              ((HomologicalComplex.coinvariantsTensorObj A (resolution k g✝⁻¹ ⋯).complex).d (j + 1) j ≫
                A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1

Tactic:
by_cases hj : Even (j + 1)

Goal state after:
case pos
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 : ℕ
a : ↑A
g : G
hj : Even (j + 1)
⊢ (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X (j + 1))).compr₂
            (ModuleCat.Hom.hom
              (A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom ≫ (moduleCatChainComplex A g✝).d (j + 1) j)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1 =
    (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X (j + 1))).compr₂
            (ModuleCat.Hom.hom
              ((HomologicalComplex.coinvariantsTensorObj A (resolution k g✝⁻¹ ⋯).complex).d (j + 1) j ≫
                A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1

case neg
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 : ℕ
a : ↑A
g : G
hj : ¬Even (j + 1)
⊢ (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X (j + 1))).compr₂
            (ModuleCat.Hom.hom
              (A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom ≫ (moduleCatChainComplex A g✝).d (j + 1) j)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1 =
    (((A.coinvariantsTensorMk ((resolution k g✝⁻¹ ⋯).complex.X (j + 1))).compr₂
            (ModuleCat.Hom.hom
              ((HomologicalComplex.coinvariantsTensorObj A (resolution k g✝⁻¹ ⋯).complex).d (j + 1) j ≫
                A.ρ.coinvariantsTprodLeftRegularLEquiv.toModuleIso.hom)))
          a ∘ₗ
        MonoidAlgebra.lsingle g)
      1
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 : ℕ
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
⊢ map (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) 1 ≫ map S.subtype (𝟙 (res S.subtype A)) 1 = 0

Tactic:
← map_comp,

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 : ℕ
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
⊢ map ((QuotientGroup.mk' S).comp S.subtype)
      ((resFunctor S.subtype).map (ofHom (A.ρ.quotientToInvariants_lift S)) ≫ 𝟙 (res S.subtype A)) 1 =
    0
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: case h.refine_3.H
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
x : ↥(cocycles₁ A)
hx :
  (ConcreteCategory.hom (H1π (res S.subtype A)))
      ((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x) =
    0
y : ↑A
hy :
  (ModuleCat.Hom.hom (d₀₁ (res S.subtype A))) y =
    ⇑((ConcreteCategory.hom (mapCocycles₁ S.subtype (𝟙 (res S.subtype A)))) x)
h1 : ∀ (g h : G), x (g * h) = (A.ρ g) (x h) + x g
h2 : ∀ s ∈ S, x s = (A.ρ s) y - y
h : G ⧸ S
g : G
⊢ Quotient.liftOn' (↑g * h) (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯ =
    ((A.quotientToInvariants S).ρ ↑g) (Quotient.liftOn' h (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯) +
      Quotient.liftOn' (↑g) (fun g ↦ ⟨↑x g - (A.ρ g) y + y, ⋯⟩) ⋯

Tactic:
| @H g =>

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)
h : η₁.hom.hom.app rightFDRep = η₂.hom.hom.app rightFDRep
this : Fintype G
⊢ η₁ = η₂

Tactic:
classical
  ext X v
  have h1 := η₁.hom.hom.naturality (ofRightFDRep X v)
  have h2 := η₂.hom.hom.naturality (ofRightFDRep X v)
  rw [h, ← h2] at h1
  simpa using congr(($h1).hom (single 1 1))

Goal state after:
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)) ⋯
inj : Function.Injective ⇑f
surj : Function.Surjective ⇑f
rkeq :
  Module.rank (IsLocalRing.ResidueField R) (maximalIdeal R).Cotangent =
    Module.rank (IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R))
      (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent
fg' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).FG
⊢ Submodule.spanFinrank (maximalIdeal (AdicCompletion (maximalIdeal R) R)) = Submodule.spanFinrank (maximalIdeal R)

Tactic:
IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg fg,

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)) ⋯
inj : Function.Injective ⇑f
surj : Function.Surjective ⇑f
rkeq :
  Module.rank (IsLocalRing.ResidueField R) (maximalIdeal R).Cotangent =
    Module.rank (IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R))
      (maximalIdeal (AdicCompletion (maximalIdeal R) R)).Cotangent
fg' : (maximalIdeal (AdicCompletion (maximalIdeal R) R)).FG
⊢ Submodule.spanFinrank (maximalIdeal (AdicCompletion (maximalIdeal R) R)) =
    Module.finrank (IsLocalRing.ResidueField R) (CotangentSpace R)
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)
⊢ map S.subtype (𝟙 (res S.subtype A)) 1 ≫ map (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv 1 = 0

Tactic:
← map_comp,

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)
⊢ map ((QuotientGroup.mk' S).comp S.subtype)
      (𝟙 (res S.subtype A) ≫ (resFunctor S.subtype).map (A.resOfQuotientIso S).inv) 1 =
    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
a b c : ℕ
σ : Type u_3
inst✝ : Finite σ
this :
  Ideal.map (toAdicCompletionAlgEquiv σ R).toRingEquiv (Ideal.span (Set.range X)) =
    Ideal.map (algebraMap (MvPolynomial σ R) (AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)))
      (MvPolynomial.idealOfVars σ R)
⊢ IsAdicComplete (MvPolynomial.idealOfVars σ R) (AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))

Tactic:
exact AdicCompletion.isAdicComplete (MvPolynomial.idealOfVars_fg σ R)

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 : ℕ
S : Subgroup G
inst✝ : S.Normal
⊢ map S.subtype (𝟙 (res S.subtype A)) 1 ≫ map (QuotientGroup.mk' S) (A.toCoinvariantsMkQ S) 1 = 0

Tactic:
← map_comp,

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
⊢ map ((QuotientGroup.mk' S).comp S.subtype) (𝟙 (res S.subtype A) ≫ (resFunctor S.subtype).map (A.toCoinvariantsMkQ S))
      1 =
    0
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ v.valuationOfNeZeroToFun 1 = 1

Tactic:
by rw [← WithZero.coe_inj, valuationOfNeZeroToFun_eq]; exact map_one _

Goal state after:
Module: Mathlib.RingTheory.Regular.IsSMulRegular

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_4
M'' : Type u_5
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup M''
inst✝ : Module R M''
r : R
f : M →ₗ[R] M'
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : f.range = g.ker
h1 : IsSMulRegular M r
h2 : IsSMulRegular M'' r
⊢ IsSMulRegular M' r

Tactic:
by
  refine IsSMulRegular.of_right_eq_zero_of_smul ?_
  intro x hx
  obtain ⟨y, ⟨⟩⟩ := (congrArg (x ∈ ·) hfg).mpr <| h2.right_eq_zero_of_smul <|
    (g.map_smul r x).symm.trans <| (congrArg _ hx).trans g.map_zero
  refine (congrArg f (h1.right_eq_zero_of_smul ?_)).trans f.map_zero
  exact hf <| (f.map_smul r y).trans <| hx.trans f.map_zero.symm

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: 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
r : R
k : ℕ
hk : (r ^ k * ↑(∏ a, g a)) • m = 0
⊢ r ^ k * ↑(∏ a, g a) ∈ Ideal.comap (algebraMap R R') p

Tactic:
rw [hx]

Goal state after:
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
r : R
k : ℕ
hk : (r ^ k * ↑(∏ a, g a)) • m = 0
⊢ r ^ k * ↑(∏ a, g a) ∈ Ideal.comap (algebraMap R R') (⊥.colon {IsLocalizedModule.mk' f m s}).radical
Module: Mathlib.RingTheory.Regular.LinearMap

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
r : R
reg : IsSMulRegular M r
mem_ann : r ∈ annihilator R N
⊢ Subsingleton (N →ₗ[R] M)

Tactic:
by
  apply subsingleton_of_forall_eq 0 (fun f ↦ ext fun x ↦ ?_)
  have : r • (f x) = r • 0 := by
    rw [smul_zero, ← map_smul, Module.mem_annihilator.mp mem_ann x, map_zero]
  simpa using reg this

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

Goal state before:
pp: case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : x ∈ ⊥
hn : n = 0
⊢ (if n = 0 then if m = 0 then 1 else 0 else 0) = if m = 0 ∧ n = 0 then ↑((m + n).choose m) else 0

pp: case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : x ∈ ⊥
hn : ¬n = 0
⊢ (if n = 0 then if m = 0 then 1 else 0 else 0) = if m = 0 ∧ n = 0 then ↑((m + n).choose m) else 0

Tactic:
· simp only [hn, ite_true, and_true, add_zero, choose_self, cast_one]

Goal state after:
case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : x ∈ ⊥
hn : ¬n = 0
⊢ (if n = 0 then if m = 0 then 1 else 0 else 0) = if m = 0 ∧ n = 0 then ↑((m + n).choose m) else 0
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
inst✝ : (x : A) → Decidable (x ∈ J)
hJ : hI.IsSubDPIdeal J
x✝² : ℕ
x✝¹ : x✝² ≠ 0
x✝ : A
ha : x✝ ∈ J
⊢ hI.dpow x✝² x✝ = (dividedPowers hI hJ).dpow x✝² x✝

Tactic:
dpow_eq_of_mem _ _ ha

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
inst✝ : (x : A) → Decidable (x ∈ J)
hJ : hI.IsSubDPIdeal J
x✝² : ℕ
x✝¹ : x✝² ≠ 0
x✝ : A
ha : x✝ ∈ J
⊢ hI.dpow x✝² x✝ = hI.dpow x✝² x✝
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case refine_2
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : ∀ {n : ℕ} {a b : A}, a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ J ⊓ I
⊢ hI.dpow n a ∈ ↑J

Tactic:
rw [← sub_zero (hI.dpow n a), ← hI.dpow_eval_zero hn]

Goal state after:
case refine_2
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : ∀ {n : ℕ} {a b : A}, a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ J ⊓ I
⊢ hI.dpow n a - hI.dpow n 0 ∈ ↑J
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case mpr.h2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x.fst ^ n = 0
⊢ ((x ^ n) ^ 2).snd = snd 0

Tactic:
rw [pow_two, snd_mul, fst_pow, hn, MulOpposite.op_zero, zero_smul, zero_smul, zero_add,
        snd_zero]

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

Goal state before:
pp: case refine_1
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ sSup (toIdeal '' S) = sSup (val '' Set.range fun a ↦ ⨆ (_ : a ∈ S), ⟨a.carrier, ⋯⟩)

Tactic:
sSup_image,

Goal state after:
case refine_1
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ ⨆ a ∈ S, ↑a = sSup (val '' Set.range fun a ↦ ⨆ (_ : a ∈ S), ⟨a.carrier, ⋯⟩)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case refine_1
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ ⨆ a ∈ S, ↑a = sSup (val '' Set.range fun a ↦ ⨆ (_ : a ∈ S), ⟨a.carrier, ⋯⟩)

Tactic:
sSup_image,

Goal state after:
case refine_1
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
⊢ ⨆ a ∈ S, ↑a = ⨆ a ∈ Set.range fun a ↦ ⨆ (_ : a ∈ S), ⟨a.carrier, ⋯⟩, ↑a
Module: Mathlib.RingTheory.Frobenius

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
G : Type u_3
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
Q : Ideal S
σ σ' : G
H : IsArithFrobAt R σ Q
H' : IsArithFrobAt R σ' Q
⊢ σ * σ'⁻¹ ∈ Ideal.inertia G Q

Tactic:
by
  intro x
  simpa [mul_smul] using sub_mem (H (σ'⁻¹ • x)) (H' (σ'⁻¹ • x))

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

Goal state before:
pp: Γ : 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
f : PowerSeries R
g : Γ
hg : g = 0
n : ℕ
hn : n ≠ 0
⊢ ((powerSeriesFamily 0 f) n).coeff 0 = 0

Tactic:
by simp [hn]

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
g : Γ
n : ℕ
hn : n ≠ 0
⊢ (if n = 0 then (if 0 < x.orderTop then x else 0) ^ n else 0).coeff g = 0

Tactic:
by simp [hn]

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
σ : Type u_7
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
r : R
g : Γ
n : ℕ
hn : n ≠ 0
⊢ (if n = 0 then r • (if 0 < x.orderTop then x else 0) ^ n else 0).coeff g = 0

Tactic:
by simp [hn]

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⟦Γ⟧
hx : 0 < x.orderTop
g : Γ
n : ℕ
hn : n ≠ 1
⊢ ({ toFun := fun a ↦ if a = 1 then x ^ a else 0, isPWO_iUnion_support' := ⋯, finite_co_support' := ⋯ } n).coeff g = 0

Tactic:
by simp [hn]

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

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_2
inst✝⁴ : AddCancelCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x y : R⟦Γ⟧
hx : ¬x = 0
hy : y = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop

Tactic:
simp [hy]

Goal state after:
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
n : ℕ
x✝ : Γ
⊢ (0 ^ n).coeff x✝ = ((single 0 1) n).coeff x✝

Tactic:
obtain rfl | ha := eq_or_ne n 0

Goal state after:
case inl
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x✝ : Γ
⊢ (0 ^ 0).coeff x✝ = ((single 0 1) 0).coeff x✝

case inr
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
n : ℕ
x✝ : Γ
ha : n ≠ 0
⊢ (0 ^ n).coeff x✝ = ((single 0 1) n).coeff x✝
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 : IsUnit x.leadingCoeff
hxo : IsAddUnit x.order
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
h : u = x.leadingCoeff
h' : (1 - (1 - (single ↑(-hxo.addUnit)) i * x)) * (SummableFamily.powers (1 - (single ↑(-hxo.addUnit)) i * x)).hsum = 1
⊢ IsUnit x

Tactic:
sub_sub_cancel

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
hx : IsUnit x.leadingCoeff
hxo : IsAddUnit x.order
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
h : u = x.leadingCoeff
h' : (single ↑(-hxo.addUnit)) i * x * (SummableFamily.powers (1 - (single ↑(-hxo.addUnit)) i * x)).hsum = 1
⊢ IsUnit x
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case mpr
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommGroup Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R⟦Γ⟧
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
hx : u = x.leadingCoeff
h : (1 - (1 - (single (-x.order)) i * x)) * (SummableFamily.powers (1 - (single (-x.order)) i * x)).hsum = 1
⊢ IsUnit x

Tactic:
sub_sub_cancel

Goal state after:
case mpr
Γ : Type u_1
R : Type u_3
inst✝⁴ : AddCommGroup Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R⟦Γ⟧
u i : R
ui : u * i = 1
iu : i * x.leadingCoeff = 1
hx : u = x.leadingCoeff
h : (single (-x.order)) i * x * (SummableFamily.powers (1 - (single (-x.order)) i * x)).hsum = 1
⊢ IsUnit x
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✝³ : AddCommGroup Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
x : R⟦Γ⟧
x0 : x ≠ 0
h :
  (1 - (1 - (single (-x.order)) x.leadingCoeff⁻¹ * x)) *
      (SummableFamily.powers (1 - (single (-x.order)) x.leadingCoeff⁻¹ * x)).hsum =
    1
⊢ x * x⁻¹ = 1

Tactic:
sub_sub_cancel

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : AddCommGroup Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
x : R⟦Γ⟧
x0 : x ≠ 0
h :
  (single (-x.order)) x.leadingCoeff⁻¹ * x *
      (SummableFamily.powers (1 - (single (-x.order)) x.leadingCoeff⁻¹ * x)).hsum =
    1
⊢ x * x⁻¹ = 1