mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Regular.IsSMulRegular

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_4
M'' : Type u_5
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup M''
inst✝ : Module R M''
r : R
f : M →ₗ[R] M'
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : f.range = g.ker
h1 : IsSMulRegular M r
h2 : IsSMulRegular M'' r
⊢ IsSMulRegular M' r

Tactic:
refine IsSMulRegular.of_right_eq_zero_of_smul ?_

Goal state after:
R : Type u_1
M : Type u_3
M' : Type u_4
M'' : Type u_5
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
inst✝¹ : AddCommGroup M''
inst✝ : Module R M''
r : R
f : M →ₗ[R] M'
g : M' →ₗ[R] M''
hf : Function.Injective ⇑f
hfg : f.range = g.ker
h1 : IsSMulRegular M r
h2 : IsSMulRegular M'' r
⊢ ∀ (m : M'), r • m = 0 → m = 0
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
x✝ : A
ha : x✝ ∈ ⊥
⊢ (if x✝ = 0 ∧ 0 = 0 then 1 else 0) = 1

Tactic:
rw [mem_bot.mp ha]
    simp only [and_self, ite_true]

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
h : (fun h ↦ h.dpow) hI = (fun h ↦ h.dpow) hI'
⊢ hI = hI'

Tactic:
ext n x

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
h : (fun h ↦ h.dpow) hI = (fun h ↦ h.dpow) hI'
n : ℕ
x : A
x✝ : x ∈ I
⊢ hI.dpow n x = hI'.dpow n x
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case pos
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
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : n = 0
⊢ dpow n 0 = ↑(#(∅.sym n))

Tactic:
hn

Goal state after:
case pos
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
hx : ∀ i ∈ ∅, x i ∈ I
n : ℕ
hn : n = 0
⊢ dpow 0 0 = ↑(#(∅.sym 0))
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
r x : A
hx : x ∈ {x | x ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n x) = hJ.dpow n (f x)}
n : ℕ
⊢ f (hI.dpow n (r * x)) = hJ.dpow n (f (r * x))

Tactic:
hI.dpow_mul hx.1,

Goal state after:
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
r x : A
hx : x ∈ {x | x ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n x) = hJ.dpow n (f x)}
n : ℕ
⊢ f (r ^ n * hI.dpow n x) = hJ.dpow n (f (r * x))
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: α : Type u_1
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
n : ℕ
r : R
m : M
⊢ hI.dpow (n, r • m).1 (g (n, r • m).2) = r ^ n • hI.dpow (n, m).1 (g (n, m).2)

Tactic:
dsimp only
      rw [LinearMap.map_smulₛₗ, RingHom.id_apply, ← algebraMap_smul A r (g m), smul_eq_mul,
        hI.dpow_mul (hg m), ← smul_eq_mul, ← map_pow, algebraMap_smul]

Goal state after:
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
S : Set A
hS : I = span S
hf : map f I ≤ J
h : ∀ {n : ℕ}, ∀ x ∈ S, f (hI.dpow n x) = hJ.dpow n (f x)
n : ℕ
x : A
hx : x ∈ I
⊢ hJ.dpow n (f x) = f (hI.dpow n x)

Tactic:
have hS' : S ⊆ ideal_from_ringHom hI hJ hf := fun y hy ↦ by
      simp only [mem_coe, ideal_from_ringHom, Submodule.mem_mk]
      exact ⟨hS ▸ subset_span hy, fun n => h y hy⟩

Goal state after:
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
S : Set A
hS : I = span S
hf : map f I ≤ J
h : ∀ {n : ℕ}, ∀ x ∈ S, f (hI.dpow n x) = hJ.dpow n (f x)
n : ℕ
x : A
hx : x ∈ I
hS' : S ⊆ ↑(hI.ideal_from_ringHom hJ hf)
⊢ hJ.dpow n (f x) = f (hI.dpow n x)
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
s : Finset ι
hs : s.Nonempty
hs' : ∀ i ∈ s, r i ∈ I
n : ℕ
⊢ hI.dpow n (∏ i ∈ s, r i) = n ! ^ (#s - 1) • ∏ i ∈ s, hI.dpow n (r i)

Tactic:
induction s using Finset.induction with
  | empty => simp_all
  | @insert a s has hrec =>
    rw [Finset.prod_insert has]
    by_cases h : s.Nonempty
    · rw [dpow_mul]
      · simp only [Finset.card_insert_of_notMem has, add_tsub_cancel_right, nsmul_eq_mul,
          Nat.cast_pow, Finset.prod_insert has,
          hrec h (fun i hi ↦ hs' i (mem_insert_of_mem hi)), ← mul_assoc]
        apply congr_arg₂ _ _ rfl
        have : #s = #s - 1 + 1 := by grind
        nth_rewrite 2 [this]
        rw [mul_comm, pow_succ, mul_assoc, hI.factorial_mul_dpow_eq_pow]
        exact hs' a (mem_insert_self a s)
      · obtain ⟨j, hj⟩ := h
        rw [Finset.prod_eq_prod_sdiff_singleton_mul hj]
        exact I.mul_mem_left _ (hs' j (mem_insert_of_mem hj))
    · simp [not_nonempty_iff_eq_empty.mp h]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
x : A
hx : x ∈ I
⊢ (if hx : x ∈ I then ⋯.choose else 0) = 1

Tactic:
simp only [dif_pos hx, ← hf.eq_iff, (Exists.choose_spec (hmem 0 hx)).2, map_one]

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective ⇑f
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ y, ∃ (_ : n ≠ 0 → y ∈ I), f y = hJ.dpow n (f x)
x : A
hx : x ∈ I
⊢ hJ.dpow 0 (f x) = 1
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J : Ideal A
inst✝ : (x : A) → Decidable (x ∈ J)
hJ : hI.IsSubDPIdeal J
x✝² : ℕ
x✝¹ : x✝² ≠ 0
x✝ : A
ha : x✝ ∈ J
⊢ hI.dpow x✝² x✝ = (dividedPowers hI hJ).dpow x✝² x✝

Tactic:
rw [dpow_eq_of_mem _ _ ha]

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.IsSubDPIdeal J
hK : hI.IsSubDPIdeal K
n : ℕ
⊢ n ≠ 0 → ∀ s ∈ ↑J ∪ ↑K, hI.dpow n s ∈ span (↑J ∪ ↑K)

Tactic:
hn

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
J K : Ideal A
hJ : hI.IsSubDPIdeal J
hK : hI.IsSubDPIdeal K
n : ℕ
hn : n ≠ 0
⊢ ∀ s ∈ ↑J ∪ ↑K, hI.dpow n s ∈ span (↑J ∪ ↑K)
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case inr
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
h✝ : Nonempty ι
n : ℕ
⊢ n ≠ 0 → ∀ {j : A}, j ∈ I ⊓ ⨅ i, J i → hI.dpow n j ∈ I ⊓ ⨅ i, J i

Tactic:
hn

Goal state after:
case inr
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
J : ι → Ideal A
hJ : ∀ (i : ι), hI.IsSubDPIdeal (J i)
h✝ : Nonempty ι
n : ℕ
hn : n ≠ 0
⊢ ∀ {j : A}, j ∈ I ⊓ ⨅ i, J i → hI.dpow n j ∈ I ⊓ ⨅ i, J i
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
      have : IsFiniteSplit R S := .of_subsingleton
      exact .of_algEquiv (TensorProduct.lid R S).symm

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

Goal state before:
pp: case refine_3
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
k : ℕ
hk : k ≠ 0
z : A
hz : z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
J : Ideal A := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ I
x y : A
hx : x ∈ Submodule.span A {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hy : y ∈ Submodule.span A {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hx_pow : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hy_pow : ∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
n : ℕ
⊢ n ≠ 0 → hI.dpow n (x + y) ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

Tactic:
hn

Goal state after:
case refine_3
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
k : ℕ
hk : k ≠ 0
z : A
hz : z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
J : Ideal A := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ I
x y : A
hx : x ∈ Submodule.span A {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hy : y ∈ Submodule.span A {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hx_pow : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hy_pow : ∀ (n : ℕ), n ≠ 0 → hI.dpow n y ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
n : ℕ
hn : n ≠ 0
⊢ hI.dpow n (x + y) ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case refine_4
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
k : ℕ
hk : k ≠ 0
z : A
hz : z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
J : Ideal A := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ I
a x : A
hx : x ∈ Submodule.span A {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hx_pow : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
n : ℕ
⊢ n ≠ 0 → hI.dpow n (a • x) ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

Tactic:
hn

Goal state after:
case refine_4
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
k : ℕ
hk : k ≠ 0
z : A
hz : z ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
J : Ideal A := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hSI : span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ I
a x : A
hx : x ∈ Submodule.span A {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
hx_pow : ∀ (n : ℕ), n ≠ 0 → hI.dpow n x ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
n : ℕ
hn : n ≠ 0
⊢ hI.dpow n (a • x) ∈ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}
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 : ℕ
⊢ hI.dpow n (a * x) = hI'.dpow n (a * x)

Tactic:
hI.dpow_mul hx.1,

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 = hI'.dpow n (a * x)
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring

Goal state before:
pp: ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
⊢ IsHomogeneous 𝒜 (Subsemiring.closure (insert 0 s))

Tactic:
refine IsHomogeneous.subsemiringClosure fun i x hx ↦ ?_

Goal state after:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
s : Set A
h : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
x : A
hx : x ∈ insert 0 s
⊢ ↑(((decompose 𝒜) x) i) ∈ insert 0 s
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✝ : Q.IsPrime
h :
  Nat.card (R ⧸ Ideal.comap (algebraMap R (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))) =
    Nat.card (R ⧸ Ideal.under R Q)
x : S
s : ↥Q.primeCompl
⊢ IsLocalization.mk' (Localization.AtPrime Q) (φ x) ⟨φ ↑s, ⋯⟩ -
      IsLocalization.mk' (Localization.AtPrime Q) (x ^ Nat.card (R ⧸ Ideal.under R Q))
        (s ^ Nat.card (R ⧸ Ideal.under R Q)) ∈
    maximalIdeal (Localization.AtPrime Q)

Tactic:
← IsLocalization.mk'_sub,

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✝ : Q.IsPrime
h :
  Nat.card (R ⧸ Ideal.comap (algebraMap R (Localization.AtPrime Q)) (maximalIdeal (Localization.AtPrime Q))) =
    Nat.card (R ⧸ Ideal.under R Q)
x : S
s : ↥Q.primeCompl
⊢ IsLocalization.mk' (Localization.AtPrime Q)
      (φ x * ↑(s ^ Nat.card (R ⧸ Ideal.under R Q)) - x ^ Nat.card (R ⧸ Ideal.under R Q) * ↑⟨φ ↑s, ⋯⟩)
      (⟨φ ↑s, ⋯⟩ * s ^ Nat.card (R ⧸ Ideal.under R Q)) ∈
    maximalIdeal (Localization.AtPrime Q)
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
G : Type u_3
inst✝³ : Group G
inst✝² : MulSemiringAction G S
inst✝¹ : SMulCommClass G R S
Q : Ideal S
σ : G
inst✝ : Q.IsPrime
h : IsArithFrobAt R σ Q
⊢ σ • Ideal.comap (MulSemiringAction.toAlgHom R S σ) Q = Q

Tactic:
Ideal.pointwise_smul_def

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
G : Type u_3
inst✝³ : Group G
inst✝² : MulSemiringAction G S
inst✝¹ : SMulCommClass G R S
Q : Ideal S
σ : G
inst✝ : Q.IsPrime
h : IsArithFrobAt R σ Q
⊢ Ideal.map (MulSemiringAction.toRingHom G S σ) (Ideal.comap (MulSemiringAction.toAlgHom R S σ) Q) = Q
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : 0 < x.orderTop
n : ℕ
⊢ ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0 → n ∈ ↑(image (fun i ↦ i.1 + i.2) (Set.Finite.toFinset ⋯))

Tactic:
hn

Goal state after:
case pos
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
⊢ n ∈ ↑(image (fun i ↦ i.1 + i.2) (Set.Finite.toFinset ⋯))
Module: Mathlib.RingTheory.HahnSeries.Binomial

Goal state before:
pp: Γ : 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
n : ℕ
⊢ (binomialFamily x r) n = 0 ^ n

Tactic:
rw [binomialFamily, powerSeriesFamily_of_not_orderTop_pos hx]

Goal state after:
Γ : 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
n : ℕ
⊢ (powerSeriesFamily 0 (PowerSeries.binomialSeries A r)) n = 0 ^ n
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : ¬0 < x.orderTop
n : ℕ
⊢ ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0 → n ∈ ↑(image (fun i ↦ i.1 + i.2) (Set.Finite.toFinset ⋯))

Tactic:
hn

Goal state after:
case neg
Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : ¬0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
⊢ n ∈ ↑(image (fun i ↦ i.1 + i.2) (Set.Finite.toFinset ⋯))
Module: Mathlib.RingTheory.HahnSeries.Binomial

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : AddCommMonoid Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : BinomialRing R
g : Γ
hg : 0 < g
r s : R
k n : ℕ
⊢ n ≠ k → ((binomialFamily (1 + (single g) r) s) n).coeff (k • g) = 0

Tactic:
hn

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : AddCommMonoid Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : BinomialRing R
g : Γ
hg : 0 < g
r s : R
k n : ℕ
hn : n ≠ k
⊢ ((binomialFamily (1 + (single g) r) s) n).coeff (k • g) = 0
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
u : R⟦X⟧ˣ
⊢ IsUnit ((heval x) ↑u)

Tactic:
refine isUnit_iff_exists_inv.mpr ?_
  use heval x u.inv
  rw [← heval_mul, Units.val_inv, map_one]

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
f : R⟦X⟧
n : ℕ
⊢ n ≠ 0 → ((powerSeriesFamily x f).coeff 0) n = 0

Tactic:
hn

Goal state after:
Γ : 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
⊢ ((powerSeriesFamily x f).coeff 0) n = 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✝⁸ : AddCommMonoid Γ
inst✝⁷ : PartialOrder Γ
inst✝⁶ : IsOrderedCancelAddMonoid Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
x✝³ x✝² : R⟦Γ⟧
x✝¹ : SummableFamily Γ' V α
x✝ : α
⊢ ((x✝³ + x✝²) • x✝¹) x✝ = (x✝³ • x✝¹ + x✝² • x✝¹) x✝

Tactic:
simp [add_smul]

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

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
n : Γ
hn : n = 1
⊢ (embDomain Nat.castOrderEmbedding (toPowerSeries.symm PowerSeries.X)).coeff n = 1

Tactic:
hn

Goal state after:
case pos
Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
n : Γ
hn : n = 1
⊢ (embDomain Nat.castOrderEmbedding (toPowerSeries.symm PowerSeries.X)).coeff 1 = 1
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
n : ℕ
g : Γ
⊢ g ∈ (x ^ n).support → g ∈ ↑(AddSubmonoid.closure x.support)

Tactic:
hn

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
x : R⟦Γ⟧
n : ℕ
g : Γ
hn : g ∈ (x ^ n).support
⊢ g ∈ ↑(AddSubmonoid.closure x.support)
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
g : Γ
n : ℕ
⊢ ¬(0 ^ n).coeff g = 0 → n = 0

Tactic:
hn

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : PartialOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : Semiring R
g : Γ
n : ℕ
hn : ¬(0 ^ n).coeff g = 0
⊢ n = 0
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
y : R
h1 : IsUnit ((a * y - 1) * 1 + 1)
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
⊢ IsUnit a ∧ IsUnit y

Tactic:
simpa using h1

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommGroup Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
a b : Γ
r s : R
⊢ (single a) r * (single (-b)) s⁻¹ = (single (a + -b)) (r * s⁻¹)

Tactic:
single_mul_single

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommGroup Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
a b : Γ
r s : R
⊢ (single (a + -b)) (r * s⁻¹) = (single (a + -b)) (r * s⁻¹)
Module: Mathlib.RingTheory.Ideal.UFD

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : UniqueFactorizationMonoid R
p : Ideal R
inst✝ : p.IsPrime
hph : p.height = 1
⊢ Submodule.IsPrincipal p

Tactic:
have hpn : p ≠ ⊥ := p.ne_bot_of_height_eq_one hph

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : UniqueFactorizationMonoid R
p : Ideal R
inst✝ : p.IsPrime
hph : p.height = 1
hpn : p ≠ ⊥
⊢ Submodule.IsPrincipal p
Module: Mathlib.RingTheory.Ideal.Pure

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.Pure
inst✝ : J.Pure
h : zeroLocus ↑I = zeroLocus ↑J
⊢ I = J

Tactic:
← I.ker_piRingHom_atPrime_eq_of_pure,

Goal state after:
R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.Pure
inst✝ : J.Pure
h : zeroLocus ↑I = zeroLocus ↑J
⊢ RingHom.ker (RingHom.pi fun p ↦ algebraMap R (Localization.AtPrime (↑p).asIdeal)) = J