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
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (A.ρ y.1) (x ((piFinTwoEquiv fun x ↦ G).symm (y.2.1, y.2.2))) -
          x ((piFinTwoEquiv fun x ↦ G).symm (y.1 * y.2.1, y.2.2)) +
        x ((piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1 * y.2.2)) -
      x ((piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1)) =
    (A.ρ ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y) 0))
        (x fun i ↦ (Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y) i.succ) +
      ∑ j,
        (-1) ^ (↑j + 1) •
          x
            (j.contractNth (fun x1 x2 ↦ x1 * x2)
              ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y)))

Tactic:
Fin.sum_univ_three

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑((inhomogeneousCochains A).X 2)
y : G × G × G
⊢ (A.ρ y.1) (x ((piFinTwoEquiv fun x ↦ G).symm (y.2.1, y.2.2))) -
          x ((piFinTwoEquiv fun x ↦ G).symm (y.1 * y.2.1, y.2.2)) +
        x ((piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1 * y.2.2)) -
      x ((piFinTwoEquiv fun x ↦ G).symm (y.1, y.2.1)) =
    (A.ρ ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y) 0))
        (x fun i ↦ (Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y) i.succ) +
      ((-1) ^ (↑0 + 1) •
            x
              (Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2)
                ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y))) +
          (-1) ^ (↑1 + 1) •
            x
              (Fin.contractNth 1 (fun x1 x2 ↦ x1 * x2)
                ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y))) +
        (-1) ^ (↑2 + 1) •
          x
            (Fin.contractNth 2 (fun x1 x2 ↦ x1 * x2)
              ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y))))
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
this : f (1, 1) + f (g, g⁻¹) = (A.ρ g) (f (g⁻¹, g)) + f (g, 1)
⊢ (A.ρ g) (f (g⁻¹, g)) - f (g, g⁻¹) = f (1, 1) - f (g, 1)

Tactic:
exact sub_eq_sub_iff_add_eq_add.2 this.symm

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : MulAction G A
f : G × G → A
hf : IsCocycle₂ f
g : G
this : f (1, 1) + f (g, g⁻¹) = g • f (g⁻¹, g) + f (g, 1)
⊢ g • f (g⁻¹, g) - f (g, g⁻¹) = f (1, 1) - f (g, 1)

Tactic:
exact sub_eq_sub_iff_add_eq_add.2 this.symm

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.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
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)
⊢ (ConcreteCategory.hom (H1π A)) x ∈
    (ModuleCat.Hom.hom (map (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) 1)).range

Tactic:
have h1 := (mem_cocycles₁_iff x).1 x.2

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
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
⊢ (ConcreteCategory.hom (H1π A)) x ∈
    (ModuleCat.Hom.hom (map (QuotientGroup.mk' S) (ofHom (A.ρ.quotientToInvariants_lift S)) 1)).range
Module: Mathlib.RingTheory.Noetherian.OfPrime

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I ↑(span {a})).FG
w✝¹ : ℕ
f : Fin w✝¹ → R
hf : span (Set.range f) = I ⊔ span {a}
w✝ : ℕ
i : Fin w✝ → R
hi : Submodule.span R (Set.range i) = Submodule.colon I ↑(span {a})
k : Fin w✝¹
⊢ f k ∈ span (Set.range f)

Tactic:
exact mem_span_range_self

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
x : G × G
g : ↑A
⊢ (ModuleCat.Hom.hom (d₂₁ A ≫ d₁₀ A) ∘ₗ lsingle x) g = (ModuleCat.Hom.hom 0 ∘ₗ lsingle x) g

Tactic:
simp [d₁₀, d₂₁, sum_add_index', sum_sub_index, sub_sub_sub_comm, add_sub_add_comm]

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
inst✝ : A.IsTrivial
g : G
a : ↑A
⊢ (H1AddEquivOfIsTrivial A)
      ((ConcreteCategory.hom (H1π A)) ((ConcreteCategory.hom (cycles₁IsoOfIsTrivial A).inv) (single g a))) =
    Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a

Tactic:
rw [H1AddEquivOfIsTrivial_apply, H1ToTensorOfIsTrivial_H1π_single g a]

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

Goal state before:
pp: case h.succ
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
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
n✝ : ℕ
hn : 0 < n✝ + 1
⊢ ↑(J ^ ((n✝ + 1) * m)) ⊆ ↑(J ^ m)

Tactic:
Nat.succ_mul

Goal state after:
case h.succ
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
V : Set R
hV : V ∈ 𝓝 0
m : ℕ
hm : ↑(J ^ m) ⊆ V
n✝ : ℕ
hn : 0 < n✝ + 1
⊢ ↑(J ^ (n✝ * m + m)) ⊆ ↑(J ^ m)
Module: Mathlib.RingTheory.AdicCompletion.RingHom

Goal state before:
pp: R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
I : Ideal S
inst✝² : IsAdicComplete I S
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : A →ₐ[R] S
H : ∀ (n : ℕ), (Quotient.mkₐ R (I ^ n)).comp f = (Quotient.mkₐ R (I ^ n)).comp g
⊢ f = g

Tactic:
rw [← AlgHom.cancel_left (f := ((ofAlgEquiv I).restrictScalars R).toAlgHom)
    (ofAlgEquiv I).injective]

Goal state after:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
I : Ideal S
inst✝² : IsAdicComplete I S
inst✝¹ : CommRing A
inst✝ : Algebra R A
f g : A →ₐ[R] S
H : ∀ (n : ℕ), (Quotient.mkₐ R (I ^ n)).comp f = (Quotient.mkₐ R (I ^ n)).comp g
⊢ (↑(AlgEquiv.restrictScalars R (ofAlgEquiv I))).comp f = (↑(AlgEquiv.restrictScalars R (ofAlgEquiv I))).comp g
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : AdicCompletion I M
hxn : ↑x n = 0
k : ℕ
h : n ≤ k + n
⊢ (powSMulQuotInclusion I M ⋯ ⊤) (↑(ofValEqZero I hxn) k) = ↑x (k + n)

Tactic:
ofValEqZero,

Goal state after:
case pos
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
x : AdicCompletion I M
hxn : ↑x n = 0
k : ℕ
h : n ≤ k + n
⊢ (powSMulQuotInclusion I M ⋯ ⊤) (↑⟨fun i ↦ ofValEqZeroAux I ⋯ hxn, ⋯⟩ k) = ↑x (k + n)
Module: Mathlib.RingTheory.Bialgebra.SymmetricAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (↑(Algebra.TensorProduct.assoc R R R (SymmetricAlgebra R M) (SymmetricAlgebra R M) (SymmetricAlgebra R M))).comp
      ((Algebra.TensorProduct.map
            (lift
              ((TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)).flip 1 ∘ₗ ι R M +
                (TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) 1 ∘ₗ ι R M))
            (AlgHom.id R (SymmetricAlgebra R M))).comp
        (lift
          ((TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)).flip 1 ∘ₗ ι R M +
            (TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) 1 ∘ₗ ι R M))) =
    (Algebra.TensorProduct.map (AlgHom.id R (SymmetricAlgebra R M))
          (lift
            ((TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)).flip 1 ∘ₗ ι R M +
              (TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) 1 ∘ₗ ι R M))).comp
      (lift
        ((TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)).flip 1 ∘ₗ ι R M +
          (TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) 1 ∘ₗ ι R M))

Tactic:
by
      ext x
      simp [Algebra.TensorProduct.one_def, TensorProduct.add_tmul, TensorProduct.tmul_add]
      abel

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✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
h : ∀ (I : Ideal A), Submodule.IsPrincipal (Ideal.map (algebraMap A B) I)
I : ↥(Ideal A)⁰
⊢ Submodule.IsPrincipal ↑(extendedIdeal A B I)

Tactic:
by simpa using h I

Goal state after:
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
n : ℕ
x : Kˣ
⊢ (fun x ↦ x • ↑n) (v.valuationOfNeZero x) = Multiplicative.toAdd (v.valuationOfNeZero ((powMonoidHom n) x))

Tactic:
by simp only [powMonoidHom_apply, map_pow, Int.toAdd_pow]; rfl

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

Goal state before:
pp: R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
⊢ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i)) = ⊤

Tactic:
rw [eq_top_iff]
  intro p hp
  clear hp
  induction p using DividedPowerAlgebra.induction_on with
  | C r =>
    simp only [Algebra.algebraMap_eq_smul_one]
    exact smul_mem _ _ (subset_span ⟨0, by simp⟩)
  | add x y hx hy => exact Submodule.add_mem _ hx hy
  | dp x k m hx =>
    have hm : m ∈ span R (Set.range v) := by simp [hv, mem_top]
    induction hm using span_induction generalizing x k with
    | zero => rw [dp_null]; split_ifs <;> simp [hx]
    | smul r m hm h => simp [dp_smul, smul_mem _ _ (h x k hx)]
    | mem y hy =>
      obtain ⟨i, rfl⟩ := hy
      induction hx using span_induction with
      | zero => simp
      | mem x hx =>
        obtain ⟨n, rfl⟩ := hx
        simp only
        rw [← n.mul_prod_erase' i _ (fun i ↦ dp_zero (m := v i)), mul_comm,
          ← mul_assoc, dp_mul, nsmul_eq_mul, mul_assoc, ← nsmul_eq_mul]
        refine smul_of_tower_mem _ _ (mem_span_of_mem ⟨Finsupp.single i k + n, ?_⟩)
        simp only
        rw [← (Finsupp.single i k + n).mul_prod_erase' i _ (fun i ↦ dp_zero (m := v i))]
        simp
      | add x y hxmem hymem hx hy =>
        rw [add_mul]
        exact Submodule.add_mem _ hx hy
      | smul r x hxmem hx =>
        rw [smul_mul_assoc]
        exact smul_mem _ _ hx
    | add m n hm_mem hn_mem hm hn =>
      rw [dp_add, mul_sum]
      apply sum_mem (fun c hc ↦ ?_)
      rw [← mul_assoc]
      exact hn (x * dp R c.1 m) c.2 (hm x c.1 hx)

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h1 : IsWeaklyRegular M [a, b]
h2 : torsionBy R M b = a • torsionBy R M b → torsionBy R M b = ⊥
⊢ IsWeaklyRegular M [b, a]

Tactic:
rw [isWeaklyRegular_cons_iff, isWeaklyRegular_singleton_iff] at h1 ⊢
  obtain ⟨ha, hb⟩ := h1
  rw [← isSMulRegular_iff_torsionBy_eq_bot] at h2
  specialize h2 (le_antisymm ?_ (smul_le_self_of_tower a (torsionBy R M b)))
  · refine le_of_eq_of_le ?_ <| smul_top_inf_eq_smul_of_isSMulRegular_on_quot <|
      ha.of_injective _ <| ker_eq_bot.mp <| ker_liftQ_eq_bot' _ (lsmul R M b) rfl
    rw [← (isSMulRegular_on_quot_iff_lsmul_comap_eq _ _).mp hb]
    exact (inf_eq_right.mpr (ker_le_comap _)).symm
  · rwa [ha.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, inf_comm, smul_comm,
      ← h2.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, and_iff_left hb]

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherian R M
rs rs' : List R
h2 : rs ~ rs'
h3 : IsWeaklyRegular M rs
h4 : ⊤ ≠ Ideal.ofList rs • ⊤
⊢ ⊤ ≠ Ideal.ofList rs' • ⊤

Tactic:
refine ne_of_ne_of_eq h4 (congrArg (Ideal.span · • ⊤) ?_)
    exact Set.ext fun _ => h2.mem_iff

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
a x : A
hx : x ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
n : ℕ
⊢ a ^ n * hI.dpow n x = a ^ n * hI'.dpow n x

Tactic:
hx.2

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
a x : A
hx : x ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
n : ℕ
⊢ a ^ n * hI'.dpow n x = a ^ n * hI'.dpow n x
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✝ : ℕ
x✝ : B
hn : n✝ ≠ 0
hx : x✝ ∈ J
⊢ dpow hI f m✝ (dpow hI f n✝ x✝) = ↑(m✝.uniformBell n✝) * dpow hI f (m✝ * n✝) x✝

Tactic:
by
    obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hx)
    simp only [dpow_apply' hI hIf, ha, hI.dpow_mem hn ha]
    rw [hI.dpow_comp hn ha, _root_.map_mul, map_natCast]

Goal state after:
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 = φ ζ
this : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
h₁ : ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q
h₂ : (∑ i_1 ∈ Finset.range k, (ζ ^ (q + k - i)) ^ i_1) * (ζ ^ (q + k - i) - 1) = (ζ ^ (q + k - i)) ^ k - 1
⊢ φ ζ = ζ ^ q

Tactic:
rw [pow_right_comm, hζ.1, one_pow, sub_self, mul_eq_zero, sub_eq_zero] at h₂

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 = φ ζ
this : ∀ (j : ℕ), 1 - ζ ^ ((q + k - i) * j) ∈ Q
h₁ : ∑ c ∈ Finset.range k, (1 - ζ ^ ((q + k - i) * c)) ∈ Q
h₂ : ∑ i_1 ∈ Finset.range k, (ζ ^ (q + k - i)) ^ i_1 = 0 ∨ ζ ^ (q + k - i) = 1
⊢ φ ζ = ζ ^ q
Module: Mathlib.RingTheory.HahnSeries.Binomial

Goal state before:
pp: case inr.right
Γ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : LinearOrder Γ
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
h✝ : Nontrivial A
⊢ (binomialFamily x r).hsum.leadingCoeff = 1

Tactic:
have : (binomialFamily x r 0).coeff 0 = 1 := by simp [hx]
      rw [← this]
      refine hsum_leadingCoeff_of_le (g := 0) (a := 0) (by simp [hx]) ?_ ?_
      · intro b g' hg'
        exact binomialFamily_mem_support hx r b hg'
      · intro b hb
        exact coeff_eq_zero_of_lt_orderTop <| binomialFamily_orderTop_pos hx r <|
        Nat.zero_lt_of_ne_zero hb

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

Goal state before:
pp: case ha
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ HasSubst ![PowerSeries.X, 0]

Tactic:
· exact HasSubst.X_zero

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

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

Tactic:
· exact HasSubst.X_zero

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:
inv_def,

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 *
      ((single (-x.order)) x.leadingCoeff⁻¹ *
        (SummableFamily.powers (1 - (single (-x.order)) x.leadingCoeff⁻¹ * x)).hsum) =
    1
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
F : IdealFilter A
I J K : Ideal A
hI : F.IsTorsionQuot I K
hJ : F.IsTorsionQuot J K
x : A
hx : x ∈ K
⊢ ∃ I_1 ∈ F, I_1 ≤ Submodule.colon (I ⊓ J) {x}

Tactic:
obtain ⟨I', hI'F, hI'x⟩ := hI x hx

Goal state after:
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
I J K : Ideal A
hI : F.IsTorsionQuot I K
hJ : F.IsTorsionQuot J K
x : A
hx : x ∈ K
I' : Ideal A
hI'F : I' ∈ F
hI'x : I' ≤ Submodule.colon I {x}
⊢ ∃ I_1 ∈ F, I_1 ≤ Submodule.colon (I ⊓ J) {x}
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
F : IdealFilter A
I J K : Ideal A
hI : F.IsTorsionQuot I K
hJ : F.IsTorsionQuot J K
⊢ F.IsTorsionQuot (I ⊓ J) K

Tactic:
by
  intro x hx
  obtain ⟨I', hI'F, hI'x⟩ := hI x hx
  obtain ⟨J', hJ'F, hJ'x⟩ := hJ x hx
  exact ⟨_, F.inf_mem hI'F hJ'F, (inf_le_inf hI'x hJ'x).trans Submodule.inf_colon.ge⟩

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.Pure
x : R
hx : x ∈ I
p : ↑(zeroLocus ↑I)
⊢ (RingHom.pi fun p ↦ algebraMap R (Localization.AtPrime (↑p).asIdeal)) x p = 0 p

Tactic:
rw [RingHom.pi_apply, Pi.zero_apply]

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.Pure
x : R
hx : x ∈ I
p : ↑(zeroLocus ↑I)
⊢ (algebraMap R (Localization.AtPrime (↑p).asIdeal)) x = 0
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
s : Finset R
n : ℕ
H :
  ∀ m < n + 1,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
hn : s.card ≤ n + 1
w✝ : IsLocalRing R
hp : maximalIdeal R ∈ (span ↑s).minimalPrimes
this : (maximalIdeal R).IsPrime
q : Ideal R
hq : q.IsPrime
hpq : q < maximalIdeal R
hq' : ∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < maximalIdeal R
⊢ ∃ x s', x ∉ s' ∧ s = insert x s' ∧ x ∉ q

Tactic:
have : ¬(s : Set R) ⊆ q := by
          rw [← span_le]
          exact fun e ↦ lt_irrefl _ ((hp.2 ⟨hq, e⟩ hpq.le).trans_lt hpq)
        obtain ⟨x, hxt, hxq⟩ := Set.not_subset.mp this
        exact ⟨x, _, fun e ↦ (Finset.mem_erase.mp e).1 rfl, (Finset.insert_erase hxt).symm, hxq⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

Goal state before:
pp: P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑(P.diagram.obj H).toProfinite.toTop
a✝ : IsOpen s
i : ↑P.toProfinite.toTop ⧸ ↑H.toOpenSubgroup
x✝ : i ∈ s
⊢ IsOpen (QuotientGroup.mk ⁻¹' {i})

Tactic:
convert! IsOpen.leftCoset H.toOpenSubgroup.isOpen' (Quotient.out i)

Goal state after:
P : ProfiniteGrp.{u}
H : OpenNormalSubgroup ↑P.toProfinite.toTop
s : Set ↑(P.diagram.obj H).toProfinite.toTop
a✝ : IsOpen s
i : ↑P.toProfinite.toTop ⧸ ↑H.toOpenSubgroup
x✝ : i ∈ s
⊢ QuotientGroup.mk ⁻¹' {i} = Quotient.out i • (↑H.toOpenSubgroup).carrier
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : x ∈ 𝔪
hn : x ∉ p₀.asIdeal
e : ↑(zeroLocus ↑p₀.asIdeal) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) := p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q✝ : Ideal R
hq : q✝ ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q✝, isPrime := ⋯ }
this : q.asIdeal.IsPrime
hxq : x ∈ q.asIdeal
hqm : q.asIdeal = 𝔪
h : (e ⟨closedPoint R, ⋯⟩).asIdeal.height ≤ 1
⊢ (e ⟨p₁, ⋯⟩).asIdeal < (e ⟨closedPoint R, ⋯⟩).asIdeal

Tactic:
simpa using h₁

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
I J I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
hIJ :
  ({I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf fun i ↦ (id i).colon Set.univ).radical =
    (J.colon Set.univ).radical
⊢ I' ∈ {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}

Tactic:
by simp [hI']

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : IsLasker R M
N : Submodule R M
⊢ ∃ t, N.IsMinimalPrimaryDecomposition t

Tactic:
obtain ⟨s, hs1, hs2⟩ := h N

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : IsLasker R M
N : Submodule R M
s : Finset (Submodule R M)
hs1 : s.inf id = N
hs2 : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
⊢ ∃ t, N.IsMinimalPrimaryDecomposition t
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
r : M
x✝ : r ∈ f n ⊓ (N + a ^ n • ⊤)
h1 : r ∈ ↑(f n)
h2 : r ∈ ↑(N + a ^ n • ⊤)
⊢ r ∈ N

Tactic:
simp only [add_eq_sup, SetLike.mem_coe, mem_sup, mem_smul_pointwise_iff_exists] at h2

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
r : M
x✝ : r ∈ f n ⊓ (N + a ^ n • ⊤)
h1 : r ∈ ↑(f n)
h2 : ∃ y ∈ N, ∃ z, (∃ b ∈ ⊤, a ^ n • b = z) ∧ y + z = r
⊢ r ∈ N