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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ coboundaries₂ A ≤ cocycles₂ A

Tactic:
rintro _ ⟨x, rfl⟩
  exact d₁₂_apply_mem_cocycles₂ x

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

Goal state before:
pp: case a
σ : 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
⊢ p ∈ m.leadingTerm ⁻¹' ↑(span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' B))

Tactic:
Set.mem_preimage,

Goal state after:
case a
σ : 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
⊢ m.leadingTerm p ∈ ↑(span ((fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) '' B))
Module: Mathlib.RingTheory.MvPolynomial.Ideal

Goal state before:
pp: case a
σ : 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
⊢ p ∈ (fun p ↦ (MvPolynomial.monomial (m.degree p)) 1) ⁻¹' ↑(span (m.leadingTerm '' B))

Tactic:
Set.mem_preimage,

Goal state after:
case a
σ : 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 ∈ ↑(span (m.leadingTerm '' B))
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: case mp
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G →₀ A
⊢ IsBoundary₁ x → ∃ y, (y.sum fun g a ↦ single g.2 a - single (g.1 * g.2) (g.1 • a) + single g.1 (g.1 • a)) = x

Tactic:
rintro ⟨y, hy⟩

Goal state after:
case mp
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G →₀ A
y : G × G →₀ A
hy : (y.sum fun g a ↦ single g.2 (g.1⁻¹ • a) - single (g.1 * g.2) a + single g.1 a) = x
⊢ ∃ y, (y.sum fun g a ↦ single g.2 a - single (g.1 * g.2) (g.1 • a) + single g.1 (g.1 • a)) = x
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: case mp
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G × G →₀ A
⊢ IsBoundary₂ x →
    ∃ y,
      (y.sum fun g a ↦
          single (g.2.1, g.2.2) a - single (g.1 * g.2.1, g.2.2) (g.1 • a) + single (g.1, g.2.1 * g.2.2) (g.1 • a) -
            single (g.1, g.2.1) (g.1 • a)) =
        x

Tactic:
rintro ⟨y, hy⟩

Goal state after:
case mp
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G × G →₀ A
y : G × G × G →₀ A
hy :
  (y.sum fun g a ↦
      single (g.2.1, g.2.2) (g.1⁻¹ • a) - single (g.1 * g.2.1, g.2.2) a + single (g.1, g.2.1 * g.2.2) a -
        single (g.1, g.2.1) a) =
    x
⊢ ∃ y,
    (y.sum fun g a ↦
        single (g.2.1, g.2.2) a - single (g.1 * g.2.1, g.2.2) (g.1 • a) + single (g.1, g.2.1 * g.2.2) (g.1 • a) -
          single (g.1, g.2.1) (g.1 • a)) =
      x
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 (⇑constantCoeff '' Set.range F)
⊢ I ≤ Submodule.span R⟦X⟧ (Set.range F)

Tactic:
← Set.range_comp

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))
⊢ I ≤ Submodule.span R⟦X⟧ (Set.range F)
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : id ↑((fun i ↦ toAddSubgroup (I ^ i • ⊤)) i) ⊆ U
⊢ ↑(I ^ i) ⊆ U

Tactic:
simpa using h

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

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

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

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

Goal state before:
pp: case right
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
⊢ ∀ s ∈ 𝓝 0, ∃ n_1, ↑((J ^ n) ^ n_1) ⊆ s

Tactic:
· intro V hV
    obtain ⟨m, hm⟩ := h.right V hV
    use m
    refine Set.Subset.trans ?_ hm
    cases n
    · exfalso
      exact Nat.not_succ_le_zero 0 hn
    rw [← pow_mul, Nat.succ_mul]
    apply Ideal.pow_le_pow_right
    apply Nat.le_add_left

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

Goal state before:
pp: σ : Type u_2
R : Type u_4
inst✝ : CommRing R
f : R⟦X⟧
i : σ
d : σ →₀ ℕ
hd : d i = 0
hf : constantCoeff f = 0
⊢ (MvPowerSeries.coeff d) ((toMvPowerSeries i) f) = 0

Tactic:
classical
  rw [toMvPowerSeries_apply, MvPowerSeries.rename_eq_subst, subst_X_comp_const,
    coeff_subst (HasSubst.X _), finsum_eq_zero_of_forall_eq_zero]
  simp only [MvPowerSeries.X_pow_eq, MvPowerSeries.coeff_monomial, smul_eq_mul, mul_ite, mul_one,
    mul_zero, ite_eq_right_iff]
  intro _ a
  subst a
  simp_all

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
⊢ H1π A ≫ map f φ 1 = mapCycles₁ f φ ≫ H1π B

Tactic:
by
  simp [H1π, Iso.inv_comp_eq, ← cyclesMap_comp_isoCycles₁_hom_assoc]

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
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)
⊢ (map I ((lsum R) fun i ↦ ↑i • LinearMap.id)) x =
    (ofPowSMul I M n) ((map I (LinearMap.codRestrict (I ^ n • ⊤) ((lsum R) fun i ↦ ↑i • LinearMap.id) ⋯)) x)

Tactic:
rw [← LinearMap.comp_apply, map_comp, LinearMap.subtype_comp_codRestrict]

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
a b c : ℕ
σ : Type u_3
inst✝ : Finite σ
⊢ Ideal.span (⇑(toAdicCompletionAlgEquiv σ R).toRingEquiv '' Set.range X) =
    Ideal.span
      (⇑(algebraMap (MvPolynomial σ R) (AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))) ''
        Set.range MvPolynomial.X)

Tactic:
← Set.range_comp

Goal state after:
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 σ
⊢ Ideal.span (Set.range (⇑(toAdicCompletionAlgEquiv σ R).toRingEquiv ∘ X)) =
    Ideal.span
      (Set.range
        (⇑(algebraMap (MvPolynomial σ R) (AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R))) ∘
          MvPolynomial.X))
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case inl
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S) (s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
z : G × G →₀ ↑A := (lmapDomain (↑A) k (Prod.map s s)) y
hz :
  (lmapDomain (↑A) k ⇑(QuotientGroup.mk' S)) ((ModuleCat.Hom.hom (d₂₁ A)) z) =
    (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y
v : G →₀ ↑A := x - (ModuleCat.Hom.hom (d₂₁ A)) z
hv : mapDomain (s ∘ QuotientGroup.mk) v = 0
e : G → G × G := fun g ↦ (s ↑g, (s ↑g)⁻¹ * g)
he : Function.Injective e
ve : G × G →₀ ↑A := mapDomain e v
w : G
hw : w ∈ ↑((v.sum fun a b ↦ single ((s ↑a)⁻¹ * a) ((A.ρ (s ↑a)⁻¹) b)) + v.sum fun a ↦ single (s ↑a)).support
hl : w ∈ (v.sum fun a b ↦ single ((s ↑a)⁻¹ * a) ((A.ρ (s ↑a)⁻¹) b)).support
t : G
left✝ : t ∈ v.support
ht : w ∈ (single ((s ↑t)⁻¹ * t) ((A.ρ (s ↑t)⁻¹) (v t))).support
⊢ w ∈ ↑S

Tactic:
apply support_single_subset at ht

Goal state after:
case inl
k G : Type u
inst✝³ : CommRing k
inst✝² : Group G
A : Rep k G
S : Subgroup G
inst✝¹ : S.Normal
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
x : G →₀ ↑A
hxc : x ∈ cycles₁ A
hx :
  (ConcreteCategory.hom (H1π (A.ofQuotient S)))
      ((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩) =
    0
y : ↑(ModuleCat.of k ((G ⧸ S) × G ⧸ S →₀ ↑(A.ofQuotient S)))
hy :
  (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y =
    ↑((ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) ⟨x, hxc⟩)
s : G ⧸ S → G
hs : ∀ (b : G ⧸ S), (QuotientGroup.mk' S) (s b) = b
hs₁ : QuotientGroup.mk ∘ s = id
z : G × G →₀ ↑A := (lmapDomain (↑A) k (Prod.map s s)) y
hz :
  (lmapDomain (↑A) k ⇑(QuotientGroup.mk' S)) ((ModuleCat.Hom.hom (d₂₁ A)) z) =
    (ModuleCat.Hom.hom (d₂₁ (A.ofQuotient S))) y
v : G →₀ ↑A := x - (ModuleCat.Hom.hom (d₂₁ A)) z
hv : mapDomain (s ∘ QuotientGroup.mk) v = 0
e : G → G × G := fun g ↦ (s ↑g, (s ↑g)⁻¹ * g)
he : Function.Injective e
ve : G × G →₀ ↑A := mapDomain e v
w : G
hw : w ∈ ↑((v.sum fun a b ↦ single ((s ↑a)⁻¹ * a) ((A.ρ (s ↑a)⁻¹) b)) + v.sum fun a ↦ single (s ↑a)).support
hl : w ∈ (v.sum fun a b ↦ single ((s ↑a)⁻¹ * a) ((A.ρ (s ↑a)⁻¹) b)).support
t : G
left✝ : t ∈ v.support
ht : w ∈ {(s ↑t)⁻¹ * t}
⊢ w ∈ ↑S
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
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
hc : ∑ a ∈ s, c a • a = d • a
ih :
  ∀ (f g : A × A → R), ∑ x ∈ s ×ˢ s, f x • x.1 ⊗ₜ[R] x.2 = ∑ x ∈ s ×ˢ s, g x • x.1 ⊗ₜ[R] x.2 → ∀ i ∈ s ×ˢ s, f i = g i
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
x : A
hx : x ∈ s
hcx : c x ≠ 0
hcy : ∀ y ∈ s, y ≠ x → c y = 0
⊢ ∀ b ∈ s, b ≠ x → c b • b = 0

Tactic:
by simp +contextual [hcy]

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.ExtendedHom

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Module.IsTorsionFree A B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
α : (FractionRing A)ˣ
⊢ (IsFractionRing.map ⋯) ↑α ≠ 0

Tactic:
simp [α.ne_zero]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h : p.contentIdeal = ⊤
⊢ Submodule.IsPrincipal ⊤

Tactic:
exact top_isPrincipal

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
⊢ (RingCon.mkₐ R (ringCon R M)) (C a) = (algebraMap R (DividedPowerAlgebra R M)) a

Tactic:
rw [← MvPolynomial.algebraMap_eq, AlgHom.commutes]

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
n : ℕ
m : M
⊢ dp R n (r • m) = r ^ n • dp R n m

Tactic:
rw [dp_def, dp_def, ← RingCon.coe_smul]

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
n : ℕ
m : M
⊢ ↑(X (n, r • m)) = ↑(r ^ n • X (n, m))
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
hJ : hI.IsSubDPIdeal J
inst✝ : (x : A) → Decidable (x ∈ J)
x✝ : A
hx : x✝ ∈ J
⊢ (if x✝ ∈ J then hI.dpow 1 x✝ else 0) = x✝

Tactic:
simp [if_pos hx, hI.dpow_one (hJ.isSubideal hx)]

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

Goal state before:
pp: case cons
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
rs : List R
h✝ : IsWeaklyRegular M rs
rs' : List R
h'' : rs ~ rs'
h' :
  ∀ (a b : R) (rs' : List R),
    a :: b :: rs' <+~ rs →
      let K := torsionBy R (M ⧸ Ideal.ofList rs' • ⊤) b;
      K = a • K → K = ⊥
rs₁ rs₂ : List R
r : R
l₁✝ l₂✝ : List R
a✝ : l₁✝ ~ l₂✝
ih :
  ∀ (rs₀ : List R),
    rs₀ ++ l₁✝ <+~ rs →
      rs₀ ++ l₂✝ <+~ rs →
        IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) l₁✝ → IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) l₂✝
rs₀ : List R
H₁ : rs₀ ++ r :: l₁✝ <+~ rs
H₃ : rs₀ ++ r :: l₂✝ <+~ rs
h : IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) (r :: l₁✝)
⊢ IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) (r :: l₂✝)

Tactic:
let e := quotOfListConsSMulTopEquivQuotSMulTopOuter M r rs₀

Goal state after:
case cons
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
rs : List R
h✝ : IsWeaklyRegular M rs
rs' : List R
h'' : rs ~ rs'
h' :
  ∀ (a b : R) (rs' : List R),
    a :: b :: rs' <+~ rs →
      let K := torsionBy R (M ⧸ Ideal.ofList rs' • ⊤) b;
      K = a • K → K = ⊥
rs₁ rs₂ : List R
r : R
l₁✝ l₂✝ : List R
a✝ : l₁✝ ~ l₂✝
ih :
  ∀ (rs₀ : List R),
    rs₀ ++ l₁✝ <+~ rs →
      rs₀ ++ l₂✝ <+~ rs →
        IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) l₁✝ → IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) l₂✝
rs₀ : List R
H₁ : rs₀ ++ r :: l₁✝ <+~ rs
H₃ : rs₀ ++ r :: l₂✝ <+~ rs
h : IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) (r :: l₁✝)
e : (M ⧸ Ideal.ofList (r :: rs₀) • ⊤) ≃ₗ[R] QuotSMulTop r (M ⧸ Ideal.ofList rs₀ • ⊤) :=
  quotOfListConsSMulTopEquivQuotSMulTopOuter M r rs₀
⊢ IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) (r :: l₂✝)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case zero
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 : A
m : ℕ
hm : m ≠ 0
⊢ hI.dpow m 0 ∈ span S

Tactic:
hI.dpow_eval_zero hm

Goal state after:
case zero
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 : A
m : ℕ
hm : m ≠ 0
⊢ 0 ∈ span S
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: case e_a
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
aux : ↑n ! = ↑n ! • 1
⊢ 1 = ((↑n !)⁻¹ * ↑n !) • 1

Tactic:
suffices (n ! : ℚ)⁻¹ * (n !) = 1 by
    rw [this, one_smul]

Goal state after:
case e_a
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
aux : ↑n ! = ↑n ! • 1
⊢ (↑n !)⁻¹ * ↑n ! = 1
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case mpr
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) = 0

Tactic:
rw [pow_mul]

Goal state after:
case mpr
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 = 0
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case inr.inr
R : Type u_1
K : Type u_2
inst✝ : DivisionRing K
⊢ Submodule.IsPrincipal ⊤

Tactic:
exact top_isPrincipal

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 hI' : DividedPowers I
n : ℕ
hn : n = 0
⊢ hI.dpow n 0 = hI'.dpow n 0

pp: case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : ¬n = 0
⊢ hI.dpow n 0 = hI'.dpow n 0

Tactic:
· rw [hn, hI.dpow_zero (zero_mem I), hI'.dpow_zero (zero_mem I)]

Goal state after:
case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : ¬n = 0
⊢ hI.dpow n 0 = hI'.dpow n 0
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
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst✝² : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst✝¹ : Algebra.IsUnramifiedAt R Q
inst✝ : IsNoetherianRing S
this : H.localize = H'.localize
x : S
⊢ φ x = ψ x

Tactic:
apply IsLocalization.injective (Localization.AtPrime Q) hQ

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
φ ψ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
H' : ψ.IsArithFrobAt Q
inst✝² : Q.IsPrime
hQ : Q.primeCompl ≤ S⁰
inst✝¹ : Algebra.IsUnramifiedAt R Q
inst✝ : IsNoetherianRing S
this : H.localize = H'.localize
x : S
⊢ (algebraMap S (Localization.AtPrime Q)) (φ x) = (algebraMap S (Localization.AtPrime Q)) (ψ x)
Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst✝¹² : DecidableEq ι
inst✝¹¹ : AddMonoid ι
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule S B
inst✝⁴ : GradedAlgebra 𝒜
inst✝³ : GradedAlgebra ℬ
inst✝² : Algebra R S
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
f : 𝒜 →ₐᵍ[R] fun x ↦ Submodule.restrictScalars R (ℬ x)
i✝ : ι
r : S
x : ↥(𝒜 i✝)
hx : ↑((toBaseChange S (𝒜 i✝)) (r ⊗ₜ[R] x)) ∈ baseChange S (𝒜 i✝)
⊢ f ↑x ∈ ℬ i✝

Tactic:
by exact f.map_mem x.2

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

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
a✝ : invOneSubPow S d = (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯)⁻¹ ^ d
⊢ ↑(Units.mkOfMulEqOne (1 - X) (mk 1) ⋯ ^ (d + 1) * invOneSubPow S (d + 1)) = 1

Tactic:
Units.val_mul,

Goal state after:
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
a✝ : invOneSubPow S d = (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯)⁻¹ ^ d
⊢ ↑(Units.mkOfMulEqOne (1 - X) (mk 1) ⋯ ^ (d + 1)) * ↑(invOneSubPow S (d + 1)) = 1
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
a✝ : invOneSubPow S d = (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯)⁻¹ ^ d
⊢ Units.mkOfMulEqOne (1 - X) (mk 1) ⋯ ^ (d + 1) * invOneSubPow S (d + 1) = 1

Tactic:
rw [← Units.val_eq_one, Units.val_mul, Units.val_pow_eq_pow_val]

Goal state after:
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
a✝ : invOneSubPow S d = (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯)⁻¹ ^ d
⊢ ↑(Units.mkOfMulEqOne (1 - X) (mk 1) ⋯) ^ (d + 1) * ↑(invOneSubPow S (d + 1)) = 1
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
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
⊢ ∃ c ∈ HasAntidiagonal.antidiagonal n,
    (PowerSeries.coeff c.1) a • (PowerSeries.coeff c.2) b • ((powers x) n).coeff g ≠ 0

Tactic:
refine exists_ne_zero_of_sum_ne_zero ?_

Goal state after:
Γ : 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
⊢ ∑ x_1 ∈ HasAntidiagonal.antidiagonal n,
      (PowerSeries.coeff x_1.1) a • (PowerSeries.coeff x_1.2) b • ((powers x) n).coeff g ≠
    0
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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [X, monomial_mul_monomial, coeff_monomial, single_left_inj (one_ne_zero : (1 : ℕ) ≠ 0)]

Goal state after:
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 : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
ab : α × β
hab : ab ∈ {ab | ((fun ab ↦ (of R).symm (s ab.1 • (of R) (t ab.2))) ab).coeff g ≠ 0}
⊢ ab ∈ ⋃ i ∈ ↑(VAddAntidiagonal g ⋯), Function.support fun i_1 ↦ (s i_1.1).coeff i.1 • (t i_1.2).coeff i.2

Tactic:
simp only [ne_eq, Set.mem_ofPred_eq] at hab
    obtain ⟨ij, hij⟩ := Finset.exists_ne_zero_of_sum_ne_zero hab
    simp only [mem_coe, mem_vaddAntidiagonal, Set.mem_iUnion, mem_support, ne_eq,
      Function.mem_support, exists_prop, Prod.exists]
    exact ⟨ij.1, ij.2, ⟨⟨ab.1, left_ne_zero_of_smul hij.2⟩, ⟨ab.2, right_ne_zero_of_smul hij.2⟩,
      ((mem_vaddAntidiagonal _ _).mp hij.1).2.2⟩, hij.2⟩

Goal state after:
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✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
g : Γ
⊢ {a | ((if 0 < x.orderTop then x else 0) ^ a).coeff g ≠ 0}.Finite

Tactic:
by
    by_cases h : 0 < x.orderTop
    · simp only [h, ↓reduceIte]
      exact pow_finite_co_support h g
    · simp only [h, ↓reduceIte]
      exact pow_finite_co_support (orderTop_zero (R := R) (Γ := Γ) ▸ WithTop.top_pos) g

Goal state after:
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 :
  (single (-x.order)) x.leadingCoeff⁻¹ * x *
      (SummableFamily.powers (1 - (single (-x.order)) x.leadingCoeff⁻¹ * x)).hsum =
    1
⊢ x * x⁻¹ = 1

Tactic:
rw [inv_def, ← mul_assoc, mul_comm x, h]

Goal state after: