mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : ℕ
e : G ≃* H
e' : ↑B ≃ₗ[k] ↑A
he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map ((↑e.symm).comp ↑e)
      ((resFunctor ↑e).map (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ }) ≫
        ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ })
      n =
    𝟙 (groupCohomology B n)

Tactic:
← groupCohomology.map_id

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✝ : ℕ
e : G ≃* H
e' : ↑B ≃ₗ[k] ↑A
he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map ((↑e.symm).comp ↑e)
      ((resFunctor ↑e).map (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ }) ≫
        ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ })
      n =
    map (MonoidHom.id G) (𝟙 B) n
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✝ : ℕ
e : G ≃* H
e' : ↑B ≃ₗ[k] ↑A
he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map ((↑e).comp ↑e.symm)
      ((resFunctor ↑e.symm).map (ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ }) ≫
        ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ })
      n =
    𝟙 (groupCohomology A n)

Tactic:
← groupCohomology.map_id

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✝ : ℕ
e : G ≃* H
e' : ↑B ≃ₗ[k] ↑A
he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map ((↑e).comp ↑e.symm)
      ((resFunctor ↑e.symm).map (ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ }) ≫
        ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ })
      n =
    map (MonoidHom.id H) (𝟙 A) n
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: 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
g✝ : G ⧸ S
g : G
s : ↥S
⊢ ((MonoidHom.comp A.ρ S.subtype) s) (↑x g - (A.ρ g) y + y) = x (↑s * g) - x ↑s - (A.ρ ↑s) ((A.ρ g) y) + (x ↑s + y)

Tactic:
by
        simp [add_eq_of_eq_sub (h2 s s.2), sub_eq_of_eq_add (h1 s g)]

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
⊢ Function.Surjective ⇑(ConcreteCategory.hom (chains₁ToCoinvariantsKer A))

Tactic:
rintro ⟨x, hx⟩

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A
hx : x ∈ Coinvariants.ker A.ρ
⊢ ∃ a, (ConcreteCategory.hom (chains₁ToCoinvariantsKer A)) a = ⟨x, hx⟩
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 : MvPolynomial σ R
⊢ (rename f) ↑p = ↑((MvPolynomial.rename f) p)

Tactic:
induction p using MvPolynomial.induction_on with

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
t : τ
h : t ∉ Set.range ⇑e
⊢ single t 1 ∉ Set.range (embDomain e)

Tactic:
rwa [mem_range_embDomain_iff, support_single _ (by simp), Finset.coe_singleton,
      Set.singleton_subset_iff]

Goal state after:
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
a : A
⊢ IsBoundary₀ G a → ∃ x, (x.sum fun g z ↦ g • z - z) = a

Tactic:
rintro ⟨x, hx⟩

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

Goal state before:
pp: case mpr
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
a : A
⊢ (∃ x, (x.sum fun g z ↦ g • z - z) = a) → IsBoundary₀ G a

Tactic:
rintro ⟨x, hx⟩

Goal state after:
case mpr
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
a : A
x : G →₀ A
hx : (x.sum fun g z ↦ g • z - z) = a
⊢ IsBoundary₀ G a
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: case mpr
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G →₀ A
⊢ (∃ 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) → IsBoundary₁ x

Tactic:
rintro ⟨x, hx⟩

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

Goal state before:
pp: case mpr
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x : G × G →₀ A
⊢ (∃ 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) →
    IsBoundary₂ x

Tactic:
rintro ⟨x, hx⟩

Goal state after:
case mpr
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
x✝ : G × G →₀ A
x : G × G × G →₀ A
hx :
  (x.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✝
⊢ IsBoundary₂ x✝
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ (∃ i ∈ I.ringFilterBasis.toAddGroupFilterBasis, id i ⊆ U) → ∃ i, True ∧ ↑(I ^ i) ⊆ U

Tactic:
rintro ⟨-, ⟨i, rfl⟩, h⟩
      replace h : ↑(I ^ i) ⊆ U := by simpa using h
      exact ⟨i, trivial, h⟩

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
U : Set R
⊢ (∃ i, True ∧ ↑(I ^ i) ⊆ U) → ∃ i ∈ I.ringFilterBasis.toAddGroupFilterBasis, id i ⊆ U

Tactic:
rintro ⟨i, -, h⟩
      exact ⟨(I ^ i : Ideal R), ⟨i, by simp⟩, h⟩

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
inst✝ : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)
⊢ Function.Surjective ⇑(ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv))

Tactic:
rintro ⟨x, hx⟩

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)
⊢ ∃ a, (ConcreteCategory.hom (mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)) a = ⟨x, hx⟩
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: case h
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)) ⟨x, hxc⟩ ∈ (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).g).ker
⊢ (ConcreteCategory.hom (H1π A)) ⟨x, hxc⟩ ∈ (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f).range

Tactic:
simp_all only [H1CoresCoinfOfTrivial_X₂, H1CoresCoinfOfTrivial_X₃, H1CoresCoinfOfTrivial_g,
    LinearMap.mem_ker, H1π_comp_map_apply (QuotientGroup.mk' S)]

Goal state after:
case h
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
⊢ (ConcreteCategory.hom (H1π A)) ⟨x, hxc⟩ ∈ (ModuleCat.Hom.hom (H1CoresCoinfOfTrivial A S).f).range
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)
H₄ : Injective ⇑(AlgebraTensorModule.assoc R R K K P Q).symm
H₅ : Injective ⇑(AlgebraTensorModule.assoc R R K K M N)
H₆ : Injective ⇑(LinearMap.rTensor (P ⊗[R] Q) (Algebra.linearMap R K))
⊢ Injective (⇑((mk R K (M ⊗[R] N)) 1) ∘ ⇑(map f g))

Tactic:
have H₇ := (TensorProduct.lid R (P ⊗[R] 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
H₅ : Injective ⇑(AlgebraTensorModule.assoc R R K K M N)
H₆ : Injective ⇑(LinearMap.rTensor (P ⊗[R] Q) (Algebra.linearMap R K))
H₇ : Injective ⇑(TensorProduct.lid R (P ⊗[R] Q)).symm
⊢ Injective (⇑((mk R K (M ⊗[R] N)) 1) ∘ ⇑(map f g))
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: case right
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
x inv✝ : R
hx : x * inv✝ = 1
inv_val✝ : inv✝ * x = 1
⊢ ¬(valuation K v) (↑(algebraMap R K) ↑{ val := x, inv := inv✝, val_inv := hx, inv_val := inv_val✝ }) < ↑1

Tactic:
change ¬v.valuation K (algebraMap R K x) < 1

Goal state after:
case right
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
x inv✝ : R
hx : x * inv✝ = 1
inv_val✝ : inv✝ * x = 1
⊢ ¬(valuation K v) ((algebraMap R K) x) < 1
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: case mpr
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
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ (powMonoidHom n).range →
    { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ fromUnit.ker

Tactic:
rintro ⟨x, hx⟩

Goal state after:
case mpr
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
x : Rˣ
hx : (powMonoidHom n) x = { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ fromUnit.ker
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
n : ℕ
hn : n ≠ 0
⊢ dp R n 0 = 0

Tactic:
by
  rw [dp_null, if_neg hn]

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

Goal state before:
pp: case pos.refine_2
A : Type u_3
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
x✝ ha : a ∈ I
⊢ ∀ {n : ℕ}, ∀ a ∈ S, (RingHom.id A) (hI.dpow n a) = hI'.dpow n ((RingHom.id A) a)

Tactic:
· intro m b hb
      simpa only [RingHom.id_apply] using (hdp b hb)

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

Goal state before:
pp: case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ (↑k.1!)⁻¹ʳ * (x ^ k.1 * ((↑k.2!)⁻¹ʳ * y ^ k.2)) = 0

Tactic:
mul_comm (x ^ k.1),

Goal state after:
case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ (↑k.1!)⁻¹ʳ * ((↑k.2!)⁻¹ʳ * y ^ k.2 * x ^ k.1) = 0
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hn : ¬n = 0
⊢ ‖(↑n !)⁻¹ʳ * ↑x ^ n‖ ≤ 1

Tactic:
apply le_trans (dpow'_norm_le_of_ne_zero p hn hx)
    rw [← zpow_neg_one, ← zpow_zero ↑p]
    gcongr
    · exact_mod_cast Nat.Prime.one_le hp.elim
    · norm_num

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

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
⊢ ∃ y, ∃ (_ : n ≠ 0 → y ∈ Ideal.span {↑p}), Coe.ringHom y = (RatAlgebra.dividedPowers ⊤).dpow n (Coe.ringHom x)

Tactic:
exact ⟨⟨dpow' p n x, dpow'_int p n hx⟩, fun hn ↦ dpow'_mem p hn hx, by
      simp [dpow', inverse_eq_inv', Coe.ringHom_apply, RatAlgebra.dpow_apply,
        Submodule.mem_top, ↓reduceIte]⟩

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ DividedPowers (Ideal.span {↑p})

Tactic:
refine ofInjective (Ideal.span {(p : ℤ_[p])}) (⊤)
    PadicInt.Coe.ringHom ((Set.injective_codRestrict Subtype.property).mp fun ⦃a₁ a₂⦄ a ↦ a)
    (RatAlgebra.dividedPowers (⊤ : Ideal ℚ_[p])) ?_ ?_
  · rw [Ideal.map_span, Set.image_singleton, map_natCast]
    simp only [Ideal.span_singleton_eq_top, isUnit_iff_ne_zero, ne_eq, cast_eq_zero]
    exact Nat.Prime.ne_zero hp.elim
  · intro n x hx
    exact ⟨⟨dpow' p n x, dpow'_int p n hx⟩, fun hn ↦ dpow'_mem p hn hx, by
      simp [dpow', inverse_eq_inv', Coe.ringHom_apply, RatAlgebra.dpow_apply,
        Submodule.mem_top, ↓reduceIte]⟩

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case refine_2
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
p y : K[ε]
hyI : y ∈ I
hy0 : y ≠ 0
⊢ ε * p ∈ I

Tactic:
obtain ⟨r, hr⟩ := hd' _ hyI hy0

Goal state after:
case refine_2
K : Type u_2
inst✝ : DivisionRing K
I : Ideal K[ε]
hb : I ≠ ⊥
ht : I ≠ ⊤
hd : ∀ x ∈ I, ε ∣ x
hd' : ∀ x ∈ I, x ≠ 0 → ∃ r, ε = r * x
p y : K[ε]
hyI : y ∈ I
hy0 : y ≠ 0
r : K[ε]
hr : ε = r * y
⊢ ε * p ∈ I
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case refine_2.inl
K : Type u_2
inst✝ : DivisionRing K
hI : Ideal.span {ε} < ⊥
⊢ ⊥ = ⊤

Tactic:
first | simp at hI | simp

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case refine_2.inr.inl
K : Type u_2
inst✝ : DivisionRing K
hI : Ideal.span {ε} < Ideal.span {ε}
⊢ Ideal.span {ε} = ⊤

Tactic:
first | simp at hI | simp

Goal state after:
Module: Mathlib.RingTheory.DualNumber

Goal state before:
pp: case refine_2.inr.inr
K : Type u_2
inst✝ : DivisionRing K
hI : Ideal.span {ε} < ⊤
⊢ ⊤ = ⊤

Tactic:
first | simp at hI | simp

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
m✝ n✝ : ℕ
a : A
ha : a ∈ I
hx : f a ∈ J
⊢ dpow hI f m✝ (f a) * dpow hI f n✝ (f a) = ↑((m✝ + n✝).choose m✝) * dpow hI f (m✝ + n✝) (f a)

Tactic:
simp only [dpow_apply' hI hIf ha]

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
m✝ n✝ : ℕ
a : A
ha : a ∈ I
hx : f a ∈ J
⊢ f (hI.dpow m✝ a) * f (hI.dpow n✝ a) = ↑((m✝ + n✝).choose m✝) * f (hI.dpow (m✝ + n✝) 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
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
inst✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
j : ℕ
⊢ ζ ^ (i * j) - ζ ^ (q * j) * ζ ^ (k * j) ∈ Q

Tactic:
pow_mul _ k,

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
inst✝ : IsDomain S
ζ : S
m : ℕ
hζ✝ : ζ ^ m = 1
hk'✝ : ↑m ∉ Q
q : ℕ := Nat.card (R ⧸ Ideal.under R Q)
hm : m ≠ 0
k : ℕ
hk : k > 0
hζ : IsPrimitiveRoot ζ k
hk' : ↑k ∉ Q
this : NeZero k
i : ℕ
hi : i < k
e : ζ ^ i = φ ζ
j : ℕ
⊢ ζ ^ (i * j) - ζ ^ (q * j) * (ζ ^ k) ^ j ∈ Q
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
x y : F.Point σ
⊢ HasSubst ![↑x, ↑y]

Tactic:
by simp [hasSubst_of_constantCoeff_nilpotent, x.prop, y.prop]

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✝¹ : AddCommMonoid R
ι : Type ?u.21
inst✝ : DecidableEq ι
i : ι
x : R⟦Γ⟧
g : Γ
j : ι
⊢ j ∈ {a | (Pi.single i x a).coeff g ≠ 0} → j ∈ {i}

Tactic:
obtain rfl | ha := eq_or_ne j i <;> simp [*]

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

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
hn : n ≠ 0
h : ¬0 < x.orderTop
⊢ ↑0 < ((powers x) n).orderTop

Tactic:
· simp [h, hn]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 0 1
hd₁ : d 1 = 0
hd₀ : d 0 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![PowerSeries.X, 0] s ^ e) = 0

pp: case neg
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 0 1
hd₁ : d 1 = 0
hd₀ : ¬d 0 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![PowerSeries.X, 0] s ^ e) = 0

Tactic:
· simp [hd₀, hd₁]

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 0 1
hd₁ : d 1 = 0
hd₀ : ¬d 0 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![PowerSeries.X, 0] s ^ e) = 0
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 : Γ'
⊢ Finite ↑{ab | ((fun ab ↦ (of R).symm (s ab.1 • (of R) (t ab.2))) ab).coeff g ≠ 0}

Tactic:
by
  apply ((VAddAntidiagonal g (Set.VAddAntidiagonal.finite_of_isPWO s.isPWO_iUnion_support
    t.isPWO_iUnion_support g)).finite_toSet.biUnion'
    (fun gh _ => hasFiniteSupport_smul s t gh)).subset _
  exact fun ab hab => by
    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.FormalGroup.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 1 1
hd₁ : d 0 = 0
hd₀ : d 1 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![0, PowerSeries.X] s ^ e) = 0

pp: case neg
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 1 1
hd₁ : d 0 = 0
hd₀ : ¬d 1 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![0, PowerSeries.X] s ^ e) = 0

Tactic:
· simp [hd₀, hd₁]

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 1 1
hd₁ : d 0 = 0
hd₀ : ¬d 1 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![0, PowerSeries.X] s ^ e) = 0
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![0, PowerSeries.X] F.toPowerSeries)
⊢ subst (fun s ↦ subst (fun x ↦ subst ![0, PowerSeries.X] F.toPowerSeries) (![0, PowerSeries.X] s)) F.toPowerSeries =
    subst ![0, subst ![0, PowerSeries.X] F.toPowerSeries] F.toPowerSeries

Tactic:
congr! 2 with d
        fin_cases d
        · simp [← PowerSeries.subst_def, ← PowerSeries.coe_substAlgHom this]
        · simp [← PowerSeries.subst_def, PowerSeries.subst_X this]

Goal state after: