mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: case mk
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
h' : hI.DPMorphism hJ
toRingHom✝ : A →+* B
ideal_comp✝ : map toRingHom✝ I ≤ J
dpow_comp✝ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝ a) = toRingHom✝ (hI.dpow n a)
hh' :
  (fun h ↦ ⇑h.toRingHom) { toRingHom := toRingHom✝, ideal_comp := ideal_comp✝, dpow_comp := dpow_comp✝ } =
    (fun h ↦ ⇑h.toRingHom) h'
⊢ { toRingHom := toRingHom✝, ideal_comp := ideal_comp✝, dpow_comp := dpow_comp✝ } = h'

Tactic:
;

Goal state after:
case mk
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
h' : hI.DPMorphism hJ
toRingHom✝ : A →+* B
ideal_comp✝ : map toRingHom✝ I ≤ J
dpow_comp✝ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝ a) = toRingHom✝ (hI.dpow n a)
hh' :
  (fun h ↦ ⇑h.toRingHom) { toRingHom := toRingHom✝, ideal_comp := ideal_comp✝, dpow_comp := dpow_comp✝ } =
    (fun h ↦ ⇑h.toRingHom) h'
⊢ { toRingHom := toRingHom✝, ideal_comp := ideal_comp✝, dpow_comp := dpow_comp✝ } = h'
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: case mk.mk
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
toRingHom✝¹ : A →+* B
ideal_comp✝¹ : map toRingHom✝¹ I ≤ J
dpow_comp✝¹ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝¹ a) = toRingHom✝¹ (hI.dpow n a)
toRingHom✝ : A →+* B
ideal_comp✝ : map toRingHom✝ I ≤ J
dpow_comp✝ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝ a) = toRingHom✝ (hI.dpow n a)
hh' :
  (fun h ↦ ⇑h.toRingHom) { toRingHom := toRingHom✝¹, ideal_comp := ideal_comp✝¹, dpow_comp := dpow_comp✝¹ } =
    (fun h ↦ ⇑h.toRingHom) { toRingHom := toRingHom✝, ideal_comp := ideal_comp✝, dpow_comp := dpow_comp✝ }
⊢ { toRingHom := toRingHom✝¹, ideal_comp := ideal_comp✝¹, dpow_comp := dpow_comp✝¹ } =
    { toRingHom := toRingHom✝, ideal_comp := ideal_comp✝, dpow_comp := dpow_comp✝ }

Tactic:
;

Goal state after:
case mk.mk
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
toRingHom✝¹ : A →+* B
ideal_comp✝¹ : map toRingHom✝¹ I ≤ J
dpow_comp✝¹ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝¹ a) = toRingHom✝¹ (hI.dpow n a)
toRingHom✝ : A →+* B
ideal_comp✝ : map toRingHom✝ I ≤ J
dpow_comp✝ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝ a) = toRingHom✝ (hI.dpow n a)
hh' :
  (fun h ↦ ⇑h.toRingHom) { toRingHom := toRingHom✝¹, ideal_comp := ideal_comp✝¹, dpow_comp := dpow_comp✝¹ } =
    (fun h ↦ ⇑h.toRingHom) { toRingHom := toRingHom✝, ideal_comp := ideal_comp✝, dpow_comp := dpow_comp✝ }
⊢ { toRingHom := toRingHom✝¹, ideal_comp := ideal_comp✝¹, dpow_comp := dpow_comp✝¹ } =
    { toRingHom := toRingHom✝, ideal_comp := ideal_comp✝, dpow_comp := dpow_comp✝ }
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: case mk.mk
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
toRingHom✝¹ : A →+* B
ideal_comp✝¹ : map toRingHom✝¹ I ≤ J
dpow_comp✝¹ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝¹ a) = toRingHom✝¹ (hI.dpow n a)
toRingHom✝ : A →+* B
ideal_comp✝ : map toRingHom✝ I ≤ J
dpow_comp✝ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝ a) = toRingHom✝ (hI.dpow n a)
hh' : ⇑toRingHom✝¹ = ⇑toRingHom✝
⊢ toRingHom✝¹ = toRingHom✝

Tactic:
;

Goal state after:
case mk.mk
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
toRingHom✝¹ : A →+* B
ideal_comp✝¹ : map toRingHom✝¹ I ≤ J
dpow_comp✝¹ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝¹ a) = toRingHom✝¹ (hI.dpow n a)
toRingHom✝ : A →+* B
ideal_comp✝ : map toRingHom✝ I ≤ J
dpow_comp✝ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝ a) = toRingHom✝ (hI.dpow n a)
hh' : ⇑toRingHom✝¹ = ⇑toRingHom✝
⊢ toRingHom✝¹ = toRingHom✝
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: case mk.mk
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
toRingHom✝¹ : A →+* B
ideal_comp✝¹ : map toRingHom✝¹ I ≤ J
dpow_comp✝¹ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝¹ a) = toRingHom✝¹ (hI.dpow n a)
toRingHom✝ : A →+* B
ideal_comp✝ : map toRingHom✝ I ≤ J
dpow_comp✝ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝ a) = toRingHom✝ (hI.dpow n a)
hh' : ⇑toRingHom✝¹ = ⇑toRingHom✝
x✝ : A
⊢ toRingHom✝¹ x✝ = toRingHom✝ x✝

Tactic:
;

Goal state after:
case mk.mk
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
toRingHom✝¹ : A →+* B
ideal_comp✝¹ : map toRingHom✝¹ I ≤ J
dpow_comp✝¹ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝¹ a) = toRingHom✝¹ (hI.dpow n a)
toRingHom✝ : A →+* B
ideal_comp✝ : map toRingHom✝ I ≤ J
dpow_comp✝ : ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (toRingHom✝ a) = toRingHom✝ (hI.dpow n a)
hh' : ⇑toRingHom✝¹ = ⇑toRingHom✝
x✝ : A
⊢ toRingHom✝¹ x✝ = toRingHom✝ x✝
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module S M₂
e : M ≃+ M₂
as : List R
bs : List S
h : List.Forall₂ (fun r s ↦ ∀ (x : M), e (r • x) = s • e x) as bs
⊢ IsWeaklyRegular M as ↔ IsWeaklyRegular M₂ bs

Tactic:
by
  conv => congr <;> rw [isWeaklyRegular_iff_Fin]
  let e' i : (M ⧸ (Ideal.ofList (as.take i) • ⊤ : Submodule R M)) ≃+
      M₂ ⧸ (Ideal.ofList (bs.take i) • ⊤ : Submodule S M₂) :=
    QuotientAddGroup.congr _ _ e <|
      AddHom.map_smul_top_toAddSubgroup_of_surjective e.surjective <|
        List.forall₂_take i h
  refine (finCongr h.length_eq).forall_congr @fun _ => (e' _).isSMulRegular_congr ?_
  exact (mkQ_surjective _).forall.mpr fun _ => congrArg (mkQ _) (h.get _ _ _)

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 : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), g m ∈ I
x✝ : M
⊢ ((lift hI g hg).toLinearMap ∘ₗ embed R M) x✝ = g x✝

Tactic:
;

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), g m ∈ I
x✝ : M
⊢ ((lift hI g hg).toLinearMap ∘ₗ embed R M) x✝ = g x✝
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
S : Type u_4
inst✝⁵ : CommSemiring S
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module S N
f : M →ₗ[R] N
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S N
x✝ : M
⊢ ((map S f).toLinearMap ∘ₗ embed R M) x✝ = (↑R (embed S N) ∘ₗ f) x✝

Tactic:
;

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
S : Type u_4
inst✝⁵ : CommSemiring S
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module S N
f : M →ₗ[R] N
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S N
x✝ : M
⊢ ((map S f).toLinearMap ∘ₗ embed R M) x✝ = (↑R (embed S N) ∘ₗ f) x✝
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 : Type u_5
inst✝³ : AddCommMonoid N
inst✝² : Module R N
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
n✝ : ℕ
m✝ : M
⊢ (map R (g ∘ₗ f)) (dp R n✝ m✝) = ((map R g).comp (map R f)) (dp R n✝ m✝)

Tactic:
;

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_5
inst✝³ : AddCommMonoid N
inst✝² : Module R N
P : Type u_6
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
n✝ : ℕ
m✝ : M
⊢ (map R (g ∘ₗ f)) (dp R n✝ m✝) = ((map R g).comp (map R f)) (dp R n✝ m✝)
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
⊢ x ^ k.1 * (y ^ k.2 * ↑(m.choose k.1)) = x ^ k.1 * (y ^ k.2 * (↑m ! * ((↑k.1!)⁻¹ʳ * (↑k.2!)⁻¹ʳ)))

Tactic:
;

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
⊢ x ^ k.1 * (y ^ k.2 * ↑(m.choose k.1)) = x ^ k.1 * (y ^ k.2 * (↑m ! * ((↑k.1!)⁻¹ʳ * (↑k.2!)⁻¹ʳ)))
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: case e_a.e_a
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) = ↑m ! * ((↑k.1!)⁻¹ʳ * (↑k.2!)⁻¹ʳ)

Tactic:
;

Goal state after:
case e_a.e_a
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) = ↑m ! * ((↑k.1!)⁻¹ʳ * (↑k.2!)⁻¹ʳ)
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
m✝ n✝ : ℕ
x✝ : B
hx : x✝ ∈ J
⊢ e (hI.dpow m✝ (e.symm x✝)) * e (hI.dpow n✝ (e.symm x✝)) = ↑((m✝ + n✝).choose m✝) * e (hI.dpow (m✝ + n✝) (e.symm x✝))

Tactic:
rw [← map_mul, hI.mul_dpow, map_mul]
    · simp only [map_natCast]
    · rwa [symm_apply_mem_of_equiv_iff, h]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
⊢ Ideal.map e.symm (Ideal.map e I) = I

Tactic:
;

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
⊢ Ideal.map e.symm (Ideal.map e I) = I
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
a : A
x✝ : a ∈ I
⊢ (ofRingEquiv ⋯ (ofRingEquiv h hI)).dpow n a = hI.dpow n a

Tactic:
;

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
a : A
x✝ : a ∈ I
⊢ (ofRingEquiv ⋯ (ofRingEquiv h hI)).dpow n a = hI.dpow n a
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hJ : DividedPowers J
n : ℕ
b : B
x✝ : b ∈ J
⊢ (ofRingEquiv h (ofRingEquiv ⋯ hJ)).dpow n b = hJ.dpow n b

Tactic:
;

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hJ : DividedPowers J
n : ℕ
b : B
x✝ : b ∈ J
⊢ (ofRingEquiv h (ofRingEquiv ⋯ hJ)).dpow n b = hJ.dpow n b
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
h2 : IsSMulRegular M b
ha : IsSMulRegular M a
hb : IsSMulRegular (QuotSMulTop a M) b
⊢ IsSMulRegular M b ∧ a • ⊤ ⊓ b • ⊤ ≤ a • b • ⊤

Tactic:
inf_comm,

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h2 : IsSMulRegular M b
ha : IsSMulRegular M a
hb : IsSMulRegular (QuotSMulTop a M) b
⊢ IsSMulRegular M b ∧ b • ⊤ ⊓ a • ⊤ ≤ a • b • ⊤
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 k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ ↑(m + k)! = ↑(k ! * (m ! * (m + k).choose m))

Tactic:
;

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 k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ ↑(m + k)! = ↑(k ! * (m ! * (m + k).choose m))
Module: Mathlib.RingTheory.DividedPowers.Padic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
⊢ ‖dpow' p n ↑x‖ ≤ (↑p)⁻¹

Tactic:
unfold dpow'
  by_cases hx0 : x = 0
  · rw [hx0]
    simp [inverse_eq_inv', coe_zero, ne_eq, hn, not_false_eq_true, zero_pow, mul_zero,
      norm_zero, inv_nonneg, cast_nonneg]
  · have hlt : (padicValNat p n.factorial : ℤ) < n := by
      exact_mod_cast padicValNat_factorial_lt_of_ne_zero p hn
    have hnorm : 0 < ‖(n ! : ℚ_[p])‖ := by
      simp only [norm_pos_iff, ne_eq, cast_eq_zero]
      exact factorial_ne_zero n
    rw [← zpow_neg_one, ← Nat.cast_one (R := ℤ), Padic.norm_le_pow_iff_norm_lt_pow_add_one]
    simp only [inverse_eq_inv', Padic.padicNormE.mul, norm_inv, _root_.norm_pow,
      padic_norm_e_of_padicInt, cast_one, Int.reduceNeg, neg_add_cancel, zpow_zero]
    rw [norm_eq_zpow_neg_valuation hx0, inv_mul_lt_one₀ hnorm, Padic.norm_eq_zpow_neg_valuation
      (cast_ne_zero.mpr n.factorial_ne_zero), ← zpow_natCast, ← zpow_mul]
    gcongr
    · exact_mod_cast Nat.Prime.one_lt hp.elim
    · simp only [neg_mul, Padic.valuation_natCast, neg_lt_neg_iff]
      apply lt_of_lt_of_le hlt
      conv_lhs => rw [← one_mul (n : ℤ)]
      gcongr
      norm_cast
      rwa [← PadicInt.mem_span_pow_iff_le_valuation x hx0, pow_one]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
⊢ ‖dpow' p n ↑x‖ ≤ (↑p)⁻¹

Tactic:
by
  unfold dpow'
  by_cases hx0 : x = 0
  · rw [hx0]
    simp [inverse_eq_inv', coe_zero, ne_eq, hn, not_false_eq_true, zero_pow, mul_zero,
      norm_zero, inv_nonneg, cast_nonneg]
  · have hlt : (padicValNat p n.factorial : ℤ) < n := by
      exact_mod_cast padicValNat_factorial_lt_of_ne_zero p hn
    have hnorm : 0 < ‖(n ! : ℚ_[p])‖ := by
      simp only [norm_pos_iff, ne_eq, cast_eq_zero]
      exact factorial_ne_zero n
    rw [← zpow_neg_one, ← Nat.cast_one (R := ℤ), Padic.norm_le_pow_iff_norm_lt_pow_add_one]
    simp only [inverse_eq_inv', Padic.padicNormE.mul, norm_inv, _root_.norm_pow,
      padic_norm_e_of_padicInt, cast_one, Int.reduceNeg, neg_add_cancel, zpow_zero]
    rw [norm_eq_zpow_neg_valuation hx0, inv_mul_lt_one₀ hnorm, Padic.norm_eq_zpow_neg_valuation
      (cast_ne_zero.mpr n.factorial_ne_zero), ← zpow_natCast, ← zpow_mul]
    gcongr
    · exact_mod_cast Nat.Prime.one_lt hp.elim
    · simp only [neg_mul, Padic.valuation_natCast, neg_lt_neg_iff]
      apply lt_of_lt_of_le hlt
      conv_lhs => rw [← one_mul (n : ℤ)]
      gcongr
      norm_cast
      rwa [← PadicInt.mem_span_pow_iff_le_valuation x hx0, pow_one]

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
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₂ rs₀ : List R
h₁₂ : rs₁ ~ rs₂
H₁ : rs₀ ++ rs₁ <+~ rs
H₃ : rs₀ ++ rs₂ <+~ rs
h : IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) rs₁
⊢ IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) rs₂

Tactic:
induction h₁₂ generalizing rs₀ with

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

Goal state before:
pp: case mk
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
q : hI.SubDPIdeal
carrier✝ : Ideal A
isSubideal✝ : carrier✝ ≤ I
dpow_mem✝ : ∀ (n : ℕ), n ≠ 0 → ∀ j ∈ carrier✝, hI.dpow n j ∈ carrier✝
h : { carrier := carrier✝, isSubideal := isSubideal✝, dpow_mem := dpow_mem✝ }.carrier = q.carrier
⊢ { carrier := carrier✝, isSubideal := isSubideal✝, dpow_mem := dpow_mem✝ } = q

Tactic:
;

Goal state after:
case mk
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
q : hI.SubDPIdeal
carrier✝ : Ideal A
isSubideal✝ : carrier✝ ≤ I
dpow_mem✝ : ∀ (n : ℕ), n ≠ 0 → ∀ j ∈ carrier✝, hI.dpow n j ∈ carrier✝
h : { carrier := carrier✝, isSubideal := isSubideal✝, dpow_mem := dpow_mem✝ }.carrier = q.carrier
⊢ { carrier := carrier✝, isSubideal := isSubideal✝, dpow_mem := dpow_mem✝ } = q
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case mk.mk
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
carrier✝¹ : Ideal A
isSubideal✝¹ : carrier✝¹ ≤ I
dpow_mem✝¹ : ∀ (n : ℕ), n ≠ 0 → ∀ j ∈ carrier✝¹, hI.dpow n j ∈ carrier✝¹
carrier✝ : Ideal A
isSubideal✝ : carrier✝ ≤ I
dpow_mem✝ : ∀ (n : ℕ), n ≠ 0 → ∀ j ∈ carrier✝, hI.dpow n j ∈ carrier✝
h :
  { carrier := carrier✝¹, isSubideal := isSubideal✝¹, dpow_mem := dpow_mem✝¹ }.carrier =
    { carrier := carrier✝, isSubideal := isSubideal✝, dpow_mem := dpow_mem✝ }.carrier
⊢ { carrier := carrier✝¹, isSubideal := isSubideal✝¹, dpow_mem := dpow_mem✝¹ } =
    { carrier := carrier✝, isSubideal := isSubideal✝, dpow_mem := dpow_mem✝ }

Tactic:
;

Goal state after:
case mk.mk
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
carrier✝¹ : Ideal A
isSubideal✝¹ : carrier✝¹ ≤ I
dpow_mem✝¹ : ∀ (n : ℕ), n ≠ 0 → ∀ j ∈ carrier✝¹, hI.dpow n j ∈ carrier✝¹
carrier✝ : Ideal A
isSubideal✝ : carrier✝ ≤ I
dpow_mem✝ : ∀ (n : ℕ), n ≠ 0 → ∀ j ∈ carrier✝, hI.dpow n j ∈ carrier✝
h :
  { carrier := carrier✝¹, isSubideal := isSubideal✝¹, dpow_mem := dpow_mem✝¹ }.carrier =
    { carrier := carrier✝, isSubideal := isSubideal✝, dpow_mem := dpow_mem✝ }.carrier
⊢ { carrier := carrier✝¹, isSubideal := isSubideal✝¹, dpow_mem := dpow_mem✝¹ } =
    { carrier := carrier✝, isSubideal := isSubideal✝, dpow_mem := dpow_mem✝ }
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
J : hI.SubDPIdeal
hJ : J ∈ S
⊢ ⊤.carrier ⊓ J.carrier = I ⊓ ↑⟨J.carrier, ⋯⟩

Tactic:
;

Goal state after:
case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
J : hI.SubDPIdeal
hJ : J ∈ S
⊢ ⊤.carrier ⊓ J.carrier = I ⊓ ↑⟨J.carrier, ⋯⟩
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
J : hI.SubDPIdeal
hJ : J ∉ S
⊢ ⊤.carrier = I

Tactic:
;

Goal state after:
case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
J : hI.SubDPIdeal
hJ : J ∉ S
⊢ ⊤.carrier = I
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: case zero
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑0
⊢ ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)

Tactic:
use R, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance

Goal state after:
case h
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑0
⊢ IsFiniteSplit R (R ⊗[R] S)
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: case succ.inl
n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n + 1)
h✝ : Subsingleton R
⊢ ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)

Tactic:
use R, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance

Goal state after:
case h
n : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n + 1)
h✝ : Subsingleton R
⊢ IsFiniteSplit R (R ⊗[R] S)
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R✝ : Type u
S✝ : Type v
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
inst✝³ : Algebra R✝ S✝
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (IsScalarTower.toAlgHom R P.Ring S).comp (IsScalarTower.toAlgHom R P.Ring P.Ring) =
    (IsScalarTower.toAlgHom R S S).comp (IsScalarTower.toAlgHom R P.Ring S)

Tactic:
;

Goal state after:
R✝ : Type u
S✝ : Type v
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
inst✝³ : Algebra R✝ S✝
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ (IsScalarTower.toAlgHom R P.Ring S).comp (IsScalarTower.toAlgHom R P.Ring P.Ring) =
    (IsScalarTower.toAlgHom R S S).comp (IsScalarTower.toAlgHom R P.Ring S)
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R✝ : Type u
S✝ : Type v
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
inst✝³ : Algebra R✝ S✝
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x✝ : P.Ring
⊢ ((IsScalarTower.toAlgHom R P.Ring S).comp (IsScalarTower.toAlgHom R P.Ring P.Ring)) x✝ =
    ((IsScalarTower.toAlgHom R S S).comp (IsScalarTower.toAlgHom R P.Ring S)) x✝

Tactic:
;

Goal state after:
R✝ : Type u
S✝ : Type v
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
inst✝³ : Algebra R✝ S✝
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x✝ : P.Ring
⊢ ((IsScalarTower.toAlgHom R P.Ring S).comp (IsScalarTower.toAlgHom R P.Ring P.Ring)) x✝ =
    ((IsScalarTower.toAlgHom R S S).comp (IsScalarTower.toAlgHom R P.Ring S)) x✝