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) +
      ((-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))))

Tactic:
simp only [sub_eq_add_neg, add_assoc, Fin.val_zero, zero_add, pow_one, neg_smul,
    one_smul, Fin.val_one, Fin.val_two, pow_succ' (-1 : k) 2, neg_sq, Nat.one_add, one_pow, mul_one]

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) +
      (-x
            (Fin.contractNth 0 (fun x1 x2 ↦ x1 * x2)
              ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y))) +
        (x
            (Fin.contractNth 1 (fun x1 x2 ↦ x1 * x2)
              ((Fin.consEquiv fun a ↦ G) (((Equiv.refl G).prodCongr (piFinTwoEquiv fun x ↦ G).symm) y))) +
          -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 : G → ↑A
⊢ f ∈ cocycles₁ A ↔ ∀ (g h : G), f (g * h) = (A.ρ g) (f h) + f g

Tactic:
mem_cocycles₁_def,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G → ↑A
⊢ (∀ (g h : G), (A.ρ g) (f h) - f (g * h) + f g = 0) ↔ ∀ (g h : G), f (g * h) = (A.ρ g) (f h) + f g
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 : G → ↑A
⊢ (∀ (g h : G), (A.ρ g) (f h) + f g - f (g * h) = 0) ↔ ∀ (g h : G), f (g * h) = (A.ρ g) (f h) + f g

Tactic:
sub_eq_zero,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G → ↑A
⊢ (∀ (g h : G), (A.ρ g) (f h) + f g = f (g * h)) ↔ ∀ (g h : G), f (g * h) = (A.ρ g) (f h) + f g
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 : G × G → ↑A
⊢ (∀ (g h j : G), (A.ρ g) (f (h, j)) - f (g * h, j) + f (g, h * j) - f (g, h) = 0) ↔
    ∀ (g h j : G), f (g * h, j) + f (g, h) = (A.ρ g) (f (h, j)) + f (g, h * j)

Tactic:
sub_eq_zero,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G × G → ↑A
⊢ (∀ (g h j : G), (A.ρ g) (f (h, j)) - f (g * h, j) + f (g, h * j) = f (g, h)) ↔
    ∀ (g h j : G), f (g * h, j) + f (g, h) = (A.ρ g) (f (h, j)) + f (g, h * j)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G →₀ ↑A
h : f ∈ boundaries₁ A
⊢ f ∈ cycles₁ A

Tactic:
rcases h with ⟨x, rfl⟩

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑(ModuleCat.of k (G × G →₀ ↑A))
⊢ (ModuleCat.Hom.hom (d₂₁ A)) x ∈ cycles₁ A
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 →₀ ↑A
h : x ∈ boundaries₂ A
⊢ x ∈ cycles₂ A

Tactic:
rcases h with ⟨x, rfl⟩

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑(ModuleCat.of k (G × G × G →₀ ↑A))
⊢ (ModuleCat.Hom.hom (d₃₂ A)) x ∈ cycles₂ A
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 : ↥(cycles₂ A)
⊢ (ConcreteCategory.hom ((inhomogeneousChains A).d 2 1)) ((ConcreteCategory.hom (chainsIso₂ A).inv) ↑x) = 0

Tactic:
by
      rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₂₁_comp_inv]
      simp

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
this✝ : (𝓝 0).IsCountablyGenerated
this : (𝓤 R).IsCountablyGenerated
H : CompleteSpace R
f : ℕ → R
hf : ∀ {m n : ℕ}, m ≤ n → f m - f n ∈ I ^ m
L : R
hL : Filter.map f Filter.atTop ≤ 𝓝 L
i : ℕ
⊢ ∃ N, ∀ (n : ℕ), N ≤ n → f n - L ∈ I ^ i

Tactic:
simpa [sub_eq_neg_add] using (hI.hasBasis_nhds L).tendsto_right_iff.mp hL i

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
top : TopologicalSpace R
inst✝ : IsTopologicalRing R
J : Ideal R
⊢ ((∀ (n : ℕ), IsOpen[top] ↑(J ^ n)) ∧ ∀ s ∈ 𝓝 0, ∃ n, ↑(J ^ n) ⊆ s) → IsAdic J

Tactic:
· rintro ⟨H₁, H₂⟩
    apply IsTopologicalAddGroup.ext
    · apply @IsTopologicalRing.to_topologicalAddGroup
    · apply (RingSubgroupsBasis.toRingFilterBasis _).toAddGroupFilterBasis.isTopologicalAddGroup
    · ext s
      let := Ideal.adic_basis J
      rw [J.hasBasis_nhds_zero_adic.mem_iff]
      constructor <;> intro H
      · rcases H₂ s H with ⟨n, h⟩
        exact ⟨n, trivial, h⟩
      · rcases H with ⟨n, -, hn⟩
        rw [mem_nhds_iff]
        exact ⟨_, hn, H₁ n, (J ^ n).zero_mem⟩

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

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

Tactic:
sub_eq_zero,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
l m n : ℕ
h : l ≤ m
h' : l ≤ n
p : MvPowerSeries σ R
x : σ →₀ ℕ
hx : degree x < l
⊢ MvPolynomial.coeff x ((truncTotal m) p) = MvPolynomial.coeff x ((truncTotal n) p)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

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

Tactic:
sub_eq_zero,

Goal state after:
σ : Type u_1
R : Type u_2
n : ℕ
inst✝¹ : CommRing R
inst✝ : Finite σ
p q : MvPowerSeries σ R
x : σ →₀ ℕ
hx : degree x < n
⊢ MvPolynomial.coeff x ((truncTotal n) (p * q)) = MvPolynomial.coeff x ((truncTotal n) p * (truncTotal n) q)
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case pos
σ✝ : Type u_1
R✝ : Type u_2
n✝ : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
n : ℕ
h : n = 0
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((truncTotal n) 1) = 1

pp: case neg
σ✝ : Type u_1
R✝ : Type u_2
n✝ : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
n : ℕ
h : n ≠ 0
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((truncTotal n) 1) = 1

Tactic:
· have := Ideal.Quotient.subsingleton_iff.mpr
        (show MvPolynomial.idealOfVars σ R ^ n = ⊤ by simp [h])
      exact Subsingleton.allEq ..

Goal state after:
case neg
σ✝ : Type u_1
R✝ : Type u_2
n✝ : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
n : ℕ
h : n ≠ 0
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((truncTotal n) 1) = 1
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

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

Tactic:
sub_eq_zero,

Goal state after:
σ✝ : Type u_1
R✝ : Type u_2
n✝ : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
n : ℕ
p : MvPolynomial σ R
x : σ →₀ ℕ
h : degree x < n
⊢ MvPolynomial.coeff x ((truncTotal n) ↑p) = MvPolynomial.coeff x p
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B : Rep k G
i : ℕ
φ : A ⟶ B
⊢ ModuleCat.Hom.hom ((chainsMap (MonoidHom.id G) φ).f i) = mapRange.linearMap (Hom.hom φ).toLinearMap

Tactic:
refine lhom_ext fun _ _ => ?_

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B : Rep k G
i : ℕ
φ : A ⟶ B
x✝¹ : Fin i → G
x✝ : ↑A
⊢ (ModuleCat.Hom.hom ((chainsMap (MonoidHom.id G) φ).f i)) (single x✝¹ x✝) =
    (mapRange.linearMap (Hom.hom φ).toLinearMap) (single x✝¹ x✝)
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 : ℕ
⊢ chainsMap₂ f φ ≫ (shortComplexH1 B).f = (shortComplexH1 A).f ≫ chainsMap₁ f φ

Tactic:
simp only [shortComplexH1]
    ext : 3
    simpa [d₂₁, map_add, map_sub, ← map_inv] using congr(single _ $((hom_comm_apply φ _ _).symm))

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Denominator

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : ¬Algebra.denominator ℤ Polynomial.X = 0
⊢ False

Tactic:
exact Polynomial.transcendental_X ℤ
    ((Algebra.isIntegral_denominator_smul _).isAlgebraic.of_smul
      (mem_nonZeroDivisors_of_ne_zero h))

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : I.FG
x : ℕ → AdicCompletion I M
m n : ℕ
hx : (eval I M m) (x m) - (eval I M m) (x n) = 0
h' : m ≤ n
⊢ ↑(x n) m = ↑(x m) m

Tactic:
sub_eq_zero,

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : I.FG
x : ℕ → AdicCompletion I M
m n : ℕ
hx : (eval I M m) (x m) = (eval I M m) (x n)
h' : m ≤ n
⊢ ↑(x n) m = ↑(x m) m
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
⊢ Epi (H1CoresCoinf A S).g

Tactic:
by
  rw [ModuleCat.epi_iff_surjective]
  intro x
  induction x using H1_induction_on with | @h x =>
/- Let `x : Z₁(G ⧸ S, A_S)`. We know `Z₁(G, A_S) ⟶ Z₁(G ⧸ S, A_S)` is surjective, so pick
`y : Z₁(G, A_S)` in the preimage of `x`. -/
  rcases (ModuleCat.epi_iff_surjective _).1
    (mapCycles₁_quotientGroupMk'_epi (A.toCoinvariants S) S) x with ⟨y, hy⟩
/- We know `C₁(G, A) ⟶ C₁(G, A_S)` is surjective, so pick `Y` in the preimage of `y`. -/
  rcases mapRange_surjective _ (map_zero _)
    (Coinvariants.mk_surjective (A.ρ.comp S.subtype)) y.1 with ⟨Y, hY⟩
/- Then `d(Y) ∈ I(S)A,` since `d(y) = 0`. -/
  have : d₁₀ _ Y ∈ Coinvariants.ker (A.ρ.comp S.subtype) := by
    have h' := congr($((mapShortComplexH1 (B := toCoinvariants A S)
      (MonoidHom.id G) (toCoinvariantsMkQ A S)).comm₂₃) Y)
    simp_all [shortComplexH1, ← Coinvariants.mk_eq_zero]
  /- Thus we can pick a representation of `d(Y)` as a sum `∑ ρ(sᵢ⁻¹)(aᵢ) - aᵢ`, `sᵢ ∈ S, aᵢ ∈ A`,
and `Y - ∑ aᵢ·sᵢ` is a cycle. -/
  rcases chains₁ToCoinvariantsKer_surjective
    (res S.subtype A) ⟨d₁₀ A Y, this⟩ with ⟨(Z : S →₀ A), hZ⟩
  have H : d₁₀ A (Y - mapDomain S.subtype Z) = 0 := by
    simpa [map_sub, sub_eq_zero, chains₁ToCoinvariantsKer, -LinearMap.sub_apply, d₁₀,
      sum_mapDomain_index_inj] using! Subtype.ext_iff.1 hZ.symm
  use H1π A ⟨Y - mapDomain S.subtype Z, H⟩
  simp only [H1CoresCoinf_X₃, H1CoresCoinf_X₂, H1CoresCoinf_g,
    Subgroup.coe_subtype, H1π_comp_map_apply]
/- Moreover, the image of `Y - ∑ aᵢ·sᵢ` in `Z₁(G ⧸ S, A_S)` is `x - ∑ aᵢ·1`, and hence differs from
`x` by a boundary, since `aᵢ·1 = d(aᵢ·(1, 1))`. -/
  refine (H1π_eq_iff _ _).2 ?_
  simpa [← hy, mapCycles₁_hom, map_sub, Rep.hom_id (res _ _), ← mapDomain_comp,
    ← mapDomain_mapRange, hY, Function.comp_def, (QuotientGroup.eq_one_iff <| Subtype.val _).2
    (Subtype.prop _)] using! Submodule.finsuppSum_mem _ _ _ _ fun _ _ ↦ single_one_mem_boundaries₁ _

Goal state after:
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 : Rˣ
⊢ ¬(valuation K v) (↑(algebraMap R K) ↑x) < ↑1

Tactic:
· obtain ⟨x, _, hx, _⟩ := x
    change ¬v.valuation K (algebraMap R K x) < 1
    apply_fun v.intValuation at hx
    rw [map_one, map_mul] at hx
    rw [not_lt, ← hx, ← mul_one <| v.valuation _ _, valuation_of_algebraMap]
    gcongr
    exact v.intValuation_le_one _

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
x✝¹ x✝ : A
hx : x✝ ∈ ⊥
⊢ (if x✝¹ * x✝ = 0 ∧ n = 0 then 1 else 0) = x✝¹ ^ n * if x✝ = 0 ∧ n = 0 then 1 else 0

Tactic:
rw [mem_bot.mp hx]

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
n : ℕ
x✝¹ x✝ : A
hx : x✝ ∈ ⊥
⊢ (if x✝¹ * 0 = 0 ∧ n = 0 then 1 else 0) = x✝¹ ^ n * if 0 = 0 ∧ n = 0 then 1 else 0
Module: Mathlib.RingTheory.DividedPowers.Basic

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

Tactic:
rw [mem_bot.mp hx]

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

Goal state before:
pp: case insert
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ {n : ℕ}, dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
⊢ ∑ i, dpow (↑i) (x a) * dpow (n - ↑i) (∑ x_1 ∈ s, x x_1) =
    ∑ k ∈ (insert a s).sym n, ∏ i ∈ insert a s, dpow (Multiset.count i ↑k) (x i)

Tactic:
ih hx',

Goal state after:
case insert
A : Type u_1
inst✝² : CommSemiring A
M : Type u_2
inst✝¹ : AddCommMonoid M
I : AddSubmonoid M
dpow : ℕ → M → A
dpow_zero : ∀ {x : M}, x ∈ I → dpow 0 x = 1
dpow_eval_zero : ∀ {n : ℕ}, n ≠ 0 → dpow n 0 = 0
ι : Type u_3
inst✝ : DecidableEq ι
x : ι → M
dpow_add : ∀ {n : ℕ} {x y : M}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ x_1 ∈ range n.succ, dpow x_1 x * dpow (n - x_1) y
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, x i ∈ I) → ∀ {n : ℕ}, dpow n (s.sum x) = ∑ k ∈ s.sym n, ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i)
hx : ∀ i ∈ insert a s, x i ∈ I
n : ℕ
hx' : ∀ i ∈ s, x i ∈ I
⊢ ∑ x_1, dpow (↑x_1) (x a) * ∑ k ∈ s.sym (n - ↑x_1), ∏ i ∈ s, dpow (Multiset.count i ↑k) (x i) =
    ∑ k ∈ (insert a s).sym n, ∏ i ∈ insert a s, dpow (Multiset.count i ↑k) (x i)
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
⊢ 0 ∈ {x | x ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n x) = hJ.dpow n (f x)}

Tactic:
by
    simp only [mem_ofPred_eq, Submodule.zero_mem, map_zero, true_and]
    intro n
    induction n with
    | zero => rw [hI.dpow_zero I.zero_mem, hJ.dpow_zero J.zero_mem, map_one]
    | succ n => rw [hI.dpow_eval_zero n.succ_ne_zero, hJ.dpow_eval_zero n.succ_ne_zero, map_zero]

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
inst✝ : Nontrivial M
h : ⊤ = Ideal.ofList [] • ⊤
⊢ False

Tactic:
rw [Ideal.ofList_nil, bot_smul, eq_comm, subsingleton_iff_bot_eq_top] at h

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
h : Subsingleton (Submodule R M)
⊢ False
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ Finset.antidiagonal m
⊢ m.choose k.1 • (x ^ k.1 * y ^ k.2) =
    ↑m ! * ((if x ∈ I then (↑k.1!)⁻¹ʳ * x ^ k.1 else 0) * if y ∈ I then (↑k.2!)⁻¹ʳ * y ^ k.2 else 0)

Tactic:
rw [if_pos hx, if_pos hy]

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

Goal state before:
pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hx0 : ¬x = 0
hlt : ↑(padicValNat p n !) < ↑n
hnorm : 0 < ‖↑n !‖
⊢ (↑p ^ (-↑x.valuation)) ^ n < ‖↑n !‖

Tactic:
Padic.norm_eq_zpow_neg_valuation
      (cast_ne_zero.mpr n.factorial_ne_zero),

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
hx0 : ¬x = 0
hlt : ↑(padicValNat p n !) < ↑n
hnorm : 0 < ‖↑n !‖
⊢ (↑p ^ (-↑x.valuation)) ^ n < ↑p ^ (-(↑n !).valuation)
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)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ (↑m !)⁻¹ʳ * ((↑k !)⁻¹ʳ ^ m * x ^ (k * m)) = ↑(m.uniformBell k) * ((↑(m * k)!)⁻¹ʳ * x ^ (m * k))

Tactic:
mul_comm k,

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)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ (↑m !)⁻¹ʳ * ((↑k !)⁻¹ʳ ^ m * x ^ (m * k)) = ↑(m.uniformBell k) * ((↑(m * k)!)⁻¹ʳ * x ^ (m * k))
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case swap
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
a b : R
t rs₀ : List R
H₁ : rs₀ ++ b :: a :: t <+~ rs
H₃ : rs₀ ++ a :: b :: t <+~ rs
h : IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) (b :: a :: t)
⊢ IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) (a :: b :: t)

Tactic:
rw [show ∀ x y z, x :: y :: z = [x, y] ++ z from fun _ _ _ => rfl,
      isWeaklyRegular_append_iff] at h ⊢

Goal state after:
case swap
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
a b : R
t rs₀ : List R
H₁ : rs₀ ++ b :: a :: t <+~ rs
H₃ : rs₀ ++ a :: b :: t <+~ rs
h :
  IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) [b, a] ∧
    IsWeaklyRegular ((M ⧸ Ideal.ofList rs₀ • ⊤) ⧸ Ideal.ofList [b, a] • ⊤) t
⊢ IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) [a, b] ∧
    IsWeaklyRegular ((M ⧸ Ideal.ofList rs₀ • ⊤) ⧸ Ideal.ofList [a, b] • ⊤) t
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 k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : n ≤ m * k
hxmk : x ^ (m * k) = 0
⊢ (↑m !)⁻¹ʳ * (↑k !)⁻¹ʳ ^ m * x ^ (k * m) = ↑(m.uniformBell k) * ((↑(m * k)!)⁻¹ʳ * x ^ (m * k))

Tactic:
mul_comm k,

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 k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : n ≤ m * k
hxmk : x ^ (m * k) = 0
⊢ (↑m !)⁻¹ʳ * (↑k !)⁻¹ʳ ^ m * x ^ (m * k) = ↑(m.uniformBell k) * ((↑(m * k)!)⁻¹ʳ * x ^ (m * k))
Module: Mathlib.RingTheory.Flat.LocallyFree

Goal state before:
pp: case inr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Flat R M
p : Ideal R
inst✝ : p.IsPrime
h :
  ∀ (m : Ideal R) [inst : m.IsMaximal],
    rankAtStalk M { asIdeal := m, isPrime := ⋯ } = rankAtStalk M { asIdeal := p, isPrime := ⋯ }
h✝ : Nontrivial R
Rₚ : Type u_1 := Localization.AtPrime p
n : ℕ := rankAtStalk M { asIdeal := p, isPrime := ⋯ }
f : (Fin n →₀ R) →ₗ[R] Fin n →₀ Rₚ := Finsupp.mapRange.linearMap (Algebra.linearMap R Rₚ)
g : M →ₗ[R] LocalizedModule.AtPrime p M := mkLinearMap p.primeCompl M
φ : (Fin n →₀ R) →ₗ[R] M
hφps : Function.Surjective ⇑((IsLocalizedModule.map p.primeCompl f g) φ)
a : R
hap : a ∉ p
hφas : Function.Surjective ⇑((map (Submonoid.powers a)) φ)
this : Free (Localization.Away a) (LocalizedModule.Away a (Fin n →₀ R))
φₐ : LocalizedModule.Away a (Fin n →₀ R) →ₗ[Localization.Away a] LocalizedModule.Away a M :=
  (map (Submonoid.powers a)) φ
m : Ideal (Localization.Away a)
x✝ : m.IsMaximal
𝔪 : Ideal R
left✝ : 𝔪.IsMaximal
hm𝔪 :
  (PrimeSpectrum.comap (algebraMap R (Localization (Submonoid.powers a))) { asIdeal := m, isPrime := ⋯ }).asIdeal ≤ 𝔪
⊢ rankAtStalk (LocalizedModule.Away a (Fin n →₀ R)) { asIdeal := m, isPrime := ⋯ } =
    rankAtStalk (LocalizedModule.Away a M) { asIdeal := m, isPrime := ⋯ }

Tactic:
simp [rankAtStalk_isBaseChange (LocalizedModule.isBaseChange (Submonoid.powers a) _),
      rankAtStalk_eq_of_le_of_finite_of_flat' M hm𝔪, h 𝔪, n]

Goal state after: