awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ (y : A) (_ : n ≠ 0 → y ∈ I), (f : (a : A) → B) y = hJ.dpow n ((f : (a : A) → B) x)
n : ℕ
x y : A
hx : x ∈ I
hy : y ∈ I
hxy : x + y ∈ I
⊢ Eq.{u_1 + 1} (α := A)
    (if hx : x + y ∈ I then
      ⋯.choose (p := fun (a : A) ↦ ∃ (_ : n ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow n ((f : (a : A) → B) (x + y)))
    else 0)
    (∑ k ∈ @Finset.antidiagonal _ instAddMonoid _ n,
      HMul.hMul (α := A)
        (if hx : x ∈ I then
          Exists.choose (p := fun (a : A) ↦
            ∃ (_ : k.1 ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow k.1 ((f : (a : A) → B) x)) ⋯
        else 0)
        (if hx : y ∈ I then
          Exists.choose (p := fun (a : A) ↦
            ∃ (_ : k.2 ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow k.2 ((f : (a : A) → B) y)) ⋯
        else 0))

Tactic:
simpa only [dif_pos hxy, dif_pos hx, dif_pos hy, ← hf.eq_iff, map_sum, map_mul,
      (Exists.choose_spec (_ : ∃ a, ∃ _, f a = _)).2, map_add]
      using hJ.dpow_add (hIJ ▸ I.mem_map_of_mem f hx) (hIJ ▸ I.mem_map_of_mem f hy)

Premises used: Exists.choose_spec, Function.Injective.eq_iff, DividedPowers.dpow_add, dif_pos, map_add, map_sum, map_mul
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ (y : A) (_ : n ≠ 0 → y ∈ I), (f : (a : A) → B) y = hJ.dpow n ((f : (a : A) → B) x)
n : ℕ
a x : A
hx : x ∈ I
⊢ a * x ∈ I

Tactic:
have hax : a * x ∈ I := Ideal.mul_mem_left _ _ hx
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ (y : A) (_ : n ≠ 0 → y ∈ I), (f : (a : A) → B) y = hJ.dpow n ((f : (a : A) → B) x)
n : ℕ
a x : A
hx : x ∈ I
hax : a * x ∈ I
⊢ (if hx : a * x ∈ I then
      ⋯.choose (p := fun (a_1 : A) ↦
        ∃ (_ : n ≠ 0 → a_1 ∈ I), (f : (a : A) → B) a_1 = hJ.dpow n ((f : (a : A) → B) (a * x)))
    else 0) =
    a ^ n *
      if hx : x ∈ I then
        ⋯.choose (p := fun (a : A) ↦ ∃ (_ : n ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow n ((f : (a : A) → B) x))
      else 0

Tactic:
simpa only [(Exists.choose_spec (_ : ∃ a, ∃ _, f a = _)).2, dif_pos hax, dif_pos hx,
    ← hf.eq_iff, map_mul, map_pow] using hJ.dpow_mul (hIJ ▸ I.mem_map_of_mem f hx)

Premises used: Exists.choose_spec, Function.Injective.eq_iff, dif_pos, map_pow, DividedPowers.dpow_mul, map_mul
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ (y : A) (_ : n ≠ 0 → y ∈ I), (f : (a : A) → B) y = hJ.dpow n ((f : (a : A) → B) x)
m n : ℕ
x : A
hx : x ∈ I
⊢ HMul.hMul (α := A)
      (if hx : x ∈ I then
        ⋯.choose (p := fun (a : A) ↦ ∃ (_ : m ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow m ((f : (a : A) → B) x))
      else 0)
      (if hx : x ∈ I then
        ⋯.choose (p := fun (a : A) ↦ ∃ (_ : n ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow n ((f : (a : A) → B) x))
      else 0) =
    HMul.hMul (α := A) (↑((m + n).choose m) : A)
      (if hx : x ∈ I then
        Exists.choose (p := fun (a : A) ↦
          ∃ (_ : m + n ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow (m + n) ((f : (a : A) → B) x)) ⋯
      else 0)

Tactic:
simpa only [dif_pos hx, ← hf.eq_iff, (Exists.choose_spec (hmem _ hx)).2,
    map_mul, map_natCast] using hJ.mul_dpow (hIJ ▸ I.mem_map_of_mem f hx)

Premises used: Exists.choose_spec, Function.Injective.eq_iff, dif_pos, DividedPowers.mul_dpow, map_mul, map_natCast
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ (y : A) (_ : n ≠ 0 → y ∈ I), (f : (a : A) → B) y = hJ.dpow n ((f : (a : A) → B) x)
n m : ℕ
x : A
hm : m ≠ 0
hx : x ∈ I
simp :
  (f : (a : A) → B)
      (if hx_1 :
          (if hx : x ∈ I then
              ⋯.choose (p := fun (a : A) ↦ ∃ (_ : m ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow m ((f : (a : A) → B) x))
            else 0) ∈
            I then
        Exists.choose (p := fun (a : A) ↦
          ∃ (_ : n ≠ 0 → a ∈ I),
            (f : (a : A) → B) a =
              hJ.dpow n
                ((f : (a : A) → B)
                  (⋯.choose (p := fun (a : A) ↦
                    ∃ (_ : m ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow m ((f : (a : A) → B) x)))))
          ⋯
      else 0) =
    HMul.hMul (α := B) (β := B) ((↑(n.uniformBell m) : B) : B)
      ((f : (a : A) → B)
          (Exists.choose (p := fun (a : A) ↦
            ∃ (_ : n * m ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow (n * m) ((f : (a : A) → B) x)) ⋯) :
        B)
⊢ (if hx :
        (if hx : x ∈ I then
            ⋯.choose (p := fun (a : A) ↦ ∃ (_ : m ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow m ((f : (a : A) → B) x))
          else 0) ∈
          I then
      ⋯.choose (p := fun (a : A) ↦
        ∃ (_ : n ≠ 0 → a ∈ I),
          (f : (a : A) → B) a =
            hJ.dpow n
              ((f : (a : A) → B)
                (if hx : x ∈ I then
                  ⋯.choose (p := fun (a : A) ↦
                    ∃ (_ : m ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow m ((f : (a : A) → B) x))
                else 0)))
    else 0) =
    HMul.hMul (α := A) (↑(n.uniformBell m) : A)
      (if hx : x ∈ I then
        Exists.choose (p := fun (a : A) ↦
          ∃ (_ : n * m ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow (n * m) ((f : (a : A) → B) x)) ⋯
      else 0)

Tactic:
simp only [dif_pos hx, ← hf.eq_iff, map_mul, map_natCast]

Premises used: Function.Injective.eq_iff, dif_pos, map_mul, map_natCast
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ (y : A) (_ : n ≠ 0 → y ∈ I), (f : (a : A) → B) y = hJ.dpow n ((f : (a : A) → B) x)
n m : ℕ
x : A
hm : m ≠ 0
hx : x ∈ I
rw :
  (f : (a : A) → B)
      (Exists.choose (p := fun (a : A) ↦
        ∃ (_ : n ≠ 0 → a ∈ I),
          (f : (a : A) → B) a =
            hJ.dpow n
              ((f : (a : A) → B)
                (⋯.choose (p := fun (a : A) ↦
                  ∃ (_ : m ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow m ((f : (a : A) → B) x)))))
        ⋯) =
    HMul.hMul (α := B) (β := B) ((↑(n.uniformBell m) : B) : B)
      ((f : (a : A) → B)
          (Exists.choose (p := fun (a : A) ↦
            ∃ (_ : n * m ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow (n * m) ((f : (a : A) → B) x)) ⋯) :
        B)
hc :
  (if hx : x ∈ I then
      ⋯.choose (p := fun (a : A) ↦ ∃ (_ : m ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow m ((f : (a : A) → B) x))
    else 0) ∈
    I
⊢ (f : (a : A) → B)
      (if hx_1 :
          (if hx : x ∈ I then
              ⋯.choose (p := fun (a : A) ↦ ∃ (_ : m ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow m ((f : (a : A) → B) x))
            else 0) ∈
            I then
        Exists.choose (p := fun (a : A) ↦
          ∃ (_ : n ≠ 0 → a ∈ I),
            (f : (a : A) → B) a =
              hJ.dpow n
                ((f : (a : A) → B)
                  (⋯.choose (p := fun (a : A) ↦
                    ∃ (_ : m ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow m ((f : (a : A) → B) x)))))
          ⋯
      else 0) =
    HMul.hMul (α := B) (β := B) ((↑(n.uniformBell m) : B) : B)
      ((f : (a : A) → B)
          (Exists.choose (p := fun (a : A) ↦
            ∃ (_ : n * m ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow (n * m) ((f : (a : A) → B) x)) ⋯) :
        B)

Tactic:
rw [dif_pos]

Premises used: dif_pos
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ (y : A) (_ : n ≠ 0 → y ∈ I), (f : (a : A) → B) y = hJ.dpow n ((f : (a : A) → B) x)
n m : ℕ
x : A
hm : m ≠ 0
hx : x ∈ I
simp : hJ.dpow n (hJ.dpow m ((f : (a : A) → B) x)) = (↑(n.uniformBell m) : B) * hJ.dpow (n * m) ((f : (a : A) → B) x)
⊢ (f : (a : A) → B)
      (Exists.choose (p := fun (a : A) ↦
        ∃ (_ : n ≠ 0 → a ∈ I),
          (f : (a : A) → B) a =
            hJ.dpow n
              ((f : (a : A) → B)
                (⋯.choose (p := fun (a : A) ↦
                  ∃ (_ : m ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow m ((f : (a : A) → B) x)))))
        ⋯) =
    HMul.hMul (α := B) (β := B) ((↑(n.uniformBell m) : B) : B)
      ((f : (a : A) → B)
          (Exists.choose (p := fun (a : A) ↦
            ∃ (_ : n * m ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow (n * m) ((f : (a : A) → B) x)) ⋯) :
        B)

Tactic:
simp only [(Exists.choose_spec (_ : ∃ a, ∃ _, f a = _)).2]

Premises used: Exists.choose_spec
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ (y : A) (_ : n ≠ 0 → y ∈ I), (f : (a : A) → B) y = hJ.dpow n ((f : (a : A) → B) x)
n m : ℕ
x : A
hm : m ≠ 0
hx : x ∈ I
⊢ hJ.dpow n (hJ.dpow m ((f : (a : A) → B) x)) = (↑(n.uniformBell m) : B) * hJ.dpow (n * m) ((f : (a : A) → B) x)

Tactic:
hJ.dpow_comp hm (hIJ ▸ I.mem_map_of_mem f hx)

Premises used: Ideal.mem_map_of_mem, DividedPowers.dpow_comp, Eq.rec
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ (y : A) (_ : n ≠ 0 → y ∈ I), (f : (a : A) → B) y = hJ.dpow n ((f : (a : A) → B) x)
n m : ℕ
x : A
hm : m ≠ 0
hx : x ∈ I
⊢ hJ.dpow n (hJ.dpow m ((f : (a : A) → B) x)) = (↑(n.uniformBell m) : B) * hJ.dpow (n * m) ((f : (a : A) → B) x)

Tactic:
exact hJ.dpow_comp hm (hIJ ▸ I.mem_map_of_mem f hx)

Premises used: DividedPowers.dpow_comp
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ (y : A) (_ : n ≠ 0 → y ∈ I), (f : (a : A) → B) y = hJ.dpow n ((f : (a : A) → B) x)
n m : ℕ
x : A
hm : m ≠ 0
hx : x ∈ I
hc : ⋯.choose (p := fun (a : A) ↦ ∃ (_ : m ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow m ((f : (a : A) → B) x)) ∈ I
⊢ (if hx : x ∈ I then
      ⋯.choose (p := fun (a : A) ↦ ∃ (_ : m ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow m ((f : (a : A) → B) x))
    else 0) ∈
    I

Tactic:
rw [dif_pos hx]

Premises used: dif_pos
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ (y : A) (_ : n ≠ 0 → y ∈ I), (f : (a : A) → B) y = hJ.dpow n ((f : (a : A) → B) x)
n m : ℕ
x : A
hm : m ≠ 0
hx : x ∈ I
⊢ ⋯.choose (p := fun (a : A) ↦ ∃ (_ : m ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow m ((f : (a : A) → B) x)) ∈ I

Tactic:
(Exists.choose_spec (hmem m hx)).1 hm

Premises used: Exists.choose_spec
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
f : A →+* B
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hJ : DividedPowers J
hIJ : Ideal.map f I = J
hmem : ∀ (n : ℕ) {x : A}, x ∈ I → ∃ (y : A) (_ : n ≠ 0 → y ∈ I), (f : (a : A) → B) y = hJ.dpow n ((f : (a : A) → B) x)
n m : ℕ
x : A
hm : m ≠ 0
hx : x ∈ I
⊢ ⋯.choose (p := fun (a : A) ↦ ∃ (_ : m ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow m ((f : (a : A) → B) x)) ∈ I

Tactic:
exact (Exists.choose_spec (hmem m hx)).1 hm

Premises used: Exists.choose_spec
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
pos : ∀ (hx0 : x = 0), ‖(↑n ! : ℚ_[p])⁻¹ʳ * (↑x : ℚ_[p]) ^ n‖ ≤ (↑p : ℝ)⁻¹
neg : ∀ (hx0 : ¬x = 0), ‖(↑n ! : ℚ_[p])⁻¹ʳ * (↑x : ℚ_[p]) ^ n‖ ≤ (↑p : ℝ)⁻¹
⊢ ‖(↑n ! : ℚ_[p])⁻¹ʳ * (↑x : ℚ_[p]) ^ n‖ ≤ (↑p : ℝ)⁻¹

Tactic:
by_cases hx0 : x = 0
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hx0 : x = 0
pos : ‖(↑n ! : ℚ_[p])⁻¹ʳ * HPow.hPow (α := ℚ_[p]) (↑0 : ℚ_[p]) n‖ ≤ (↑p : ℝ)⁻¹
⊢ ‖(↑n ! : ℚ_[p])⁻¹ʳ * (↑x : ℚ_[p]) ^ n‖ ≤ (↑p : ℝ)⁻¹

Tactic:
rw [hx0]
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hx0 : x = 0
⊢ ‖(↑n ! : ℚ_[p])⁻¹ʳ * HPow.hPow (α := ℚ_[p]) (↑0 : ℚ_[p]) n‖ ≤ (↑p : ℝ)⁻¹

Tactic:
simp [inverse_eq_inv', coe_zero, ne_eq, hn, not_false_eq_true, zero_pow, mul_zero,
      norm_zero, inv_nonneg, cast_nonneg]

Premises used: PadicInt.coe_zero, Ring.inverse_eq_inv', Nat.cast_nonneg, norm_zero, ne_eq, MulZeroClass.mul_zero, inv_nonneg, not_false_eq_true, zero_pow
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hx0 : ¬x = 0
⊢ LT.lt (α := ℤ) (↑(padicValNat p n !) : ℤ) (↑n : ℤ)

Tactic:
exact_mod_cast padicValNat_factorial_lt_of_ne_zero p hn

Premises used: padicValNat_factorial_lt_of_ne_zero
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hx0 : ¬x = 0
⊢ LT.lt (α := ℤ) (↑(padicValNat p n !) : ℤ) (↑n : ℤ)

Tactic:
have hlt : (padicValNat p n.factorial : ℤ) < n := by
      exact_mod_cast padicValNat_factorial_lt_of_ne_zero p hn
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hx0 : ¬x = 0
hlt : LT.lt (α := ℤ) (↑(padicValNat p n !) : ℤ) (↑n : ℤ)
simp : ¬n ! = 0
⊢ 0 < norm (E := ℚ_[p]) (↑n ! : ℚ_[p])

Tactic:
simp only [norm_pos_iff, ne_eq, cast_eq_zero]

Premises used: norm_pos_iff, ne_eq, Nat.cast_eq_zero
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hx0 : ¬x = 0
hlt : LT.lt (α := ℤ) (↑(padicValNat p n !) : ℤ) (↑n : ℤ)
⊢ ¬n ! = 0

Tactic:
factorial_ne_zero n

Premises used: Nat.factorial_ne_zero
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hx0 : ¬x = 0
hlt : LT.lt (α := ℤ) (↑(padicValNat p n !) : ℤ) (↑n : ℤ)
⊢ ¬n ! = 0

Tactic:
exact factorial_ne_zero n

Premises used: Nat.factorial_ne_zero
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hx0 : ¬x = 0
hlt : LT.lt (α := ℤ) (↑(padicValNat p n !) : ℤ) (↑n : ℤ)
⊢ 0 < norm (E := ℚ_[p]) (↑n ! : ℚ_[p])

Tactic:
have hnorm : 0 < ‖(n ! : ℚ_[p])‖ := by
      simp only [norm_pos_iff, ne_eq, cast_eq_zero]
      exact factorial_ne_zero n
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hx0 : ¬x = 0
hlt : LT.lt (α := ℤ) (↑(padicValNat p n !) : ℤ) (↑n : ℤ)
hnorm : 0 < norm (E := ℚ_[p]) (↑n ! : ℚ_[p])
neg : ‖(↑n ! : ℚ_[p])⁻¹ʳ * (↑x : ℚ_[p]) ^ n‖ < HPow.hPow (α := ℝ) (↑p : ℝ) (HAdd.hAdd (α := ℤ) (-(↑1 : ℤ)) 1)
⊢ ‖(↑n ! : ℚ_[p])⁻¹ʳ * (↑x : ℚ_[p]) ^ n‖ ≤ (↑p : ℝ)⁻¹

Tactic:
rw [← zpow_neg_one, ← Nat.cast_one (R := ℤ), Padic.norm_le_pow_iff_norm_lt_pow_add_one]

Premises used: zpow_neg_one, Padic.norm_le_pow_iff_norm_lt_pow_add_one, Nat.cast_one
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hx0 : ¬x = 0
hlt : LT.lt (α := ℤ) (↑(padicValNat p n !) : ℤ) (↑n : ℤ)
hnorm : 0 < norm (E := ℚ_[p]) (↑n ! : ℚ_[p])
neg : (norm (E := ℚ_[p]) (↑n ! : ℚ_[p]))⁻¹ * ‖x‖ ^ n < 1
⊢ ‖(↑n ! : ℚ_[p])⁻¹ʳ * (↑x : ℚ_[p]) ^ n‖ < HPow.hPow (α := ℝ) (↑p : ℝ) (HAdd.hAdd (α := ℤ) (-(↑1 : ℤ)) 1)

Tactic:
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]

Premises used: Ring.inverse_eq_inv', PadicInt.padic_norm_e_of_padicInt, norm_pow, Int.reduceNeg, zpow_zero, norm_inv, neg_add_cancel, Padic.padicNormE.mul, Nat.cast_one
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hx0 : ¬x = 0
hlt : LT.lt (α := ℤ) (↑(padicValNat p n !) : ℤ) (↑n : ℤ)
hnorm : 0 < norm (E := ℚ_[p]) (↑n ! : ℚ_[p])
neg :
  HPow.hPow (α := ℝ) (↑p : ℝ) (HMul.hMul (α := ℤ) (-(↑x.valuation : ℤ)) (↑n : ℤ)) <
    HPow.hPow (α := ℝ) (↑p : ℝ) (-Padic.valuation (p := p) (↑n ! : ℚ_[p]))
⊢ (norm (E := ℚ_[p]) (↑n ! : ℚ_[p]))⁻¹ * ‖x‖ ^ n < 1

Tactic:
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]

Premises used: zpow_natCast, Iff.mpr, inv_mul_lt_one₀, zpow_mul, PadicInt.norm_eq_zpow_neg_valuation, Padic.norm_eq_zpow_neg_valuation, Nat.factorial_ne_zero, Nat.cast_ne_zero
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hx0 : ¬x = 0
hlt : LT.lt (α := ℤ) (↑(padicValNat p n !) : ℤ) (↑n : ℤ)
hnorm : 0 < norm (E := ℚ_[p]) (↑n ! : ℚ_[p])
neg : LT.lt (α := ℝ) 1 (↑p : ℝ)
neg₁ : HMul.hMul (α := ℤ) (-(↑x.valuation : ℤ)) (↑n : ℤ) < -Padic.valuation (p := p) (↑n ! : ℚ_[p])
⊢ HPow.hPow (α := ℝ) (↑p : ℝ) (HMul.hMul (α := ℤ) (-(↑x.valuation : ℤ)) (↑n : ℤ)) <
    HPow.hPow (α := ℝ) (↑p : ℝ) (-Padic.valuation (p := p) (↑n ! : ℚ_[p]))

Tactic:
gcongr
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hx0 : ¬x = 0
hlt : LT.lt (α := ℤ) (↑(padicValNat p n !) : ℤ) (↑n : ℤ)
hnorm : 0 < norm (E := ℚ_[p]) (↑n ! : ℚ_[p])
⊢ LT.lt (α := ℝ) 1 (↑p : ℝ)

Tactic:
exact_mod_cast Nat.Prime.one_lt hp.elim

Premises used: Nat.Prime.one_lt, Fact.elim
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hx0 : ¬x = 0
hlt : LT.lt (α := ℤ) (↑(padicValNat p n !) : ℤ) (↑n : ℤ)
hnorm : 0 < norm (E := ℚ_[p]) (↑n ! : ℚ_[p])
neg : (↑(padicValNat p n !) : ℤ) < HMul.hMul (α := ℤ) (↑x.valuation : ℤ) (↑n : ℤ)
⊢ HMul.hMul (α := ℤ) (-(↑x.valuation : ℤ)) (↑n : ℤ) < -Padic.valuation (p := p) (↑n ! : ℚ_[p])

Tactic:
simp only [neg_mul, Padic.valuation_natCast, neg_lt_neg_iff]

Premises used: neg_lt_neg_iff, neg_mul, Padic.valuation_natCast
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hx0 : ¬x = 0
hlt : LT.lt (α := ℤ) (↑(padicValNat p n !) : ℤ) (↑n : ℤ)
hnorm : 0 < norm (E := ℚ_[p]) (↑n ! : ℚ_[p])
neg : (↑n : ℤ) ≤ HMul.hMul (α := ℤ) (↑x.valuation : ℤ) (↑n : ℤ)
⊢ (↑(padicValNat p n !) : ℤ) < HMul.hMul (α := ℤ) (↑x.valuation : ℤ) (↑n : ℤ)

Tactic:
apply lt_of_lt_of_le hlt

Premises used: lt_of_lt_of_le
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hx0 : ¬x = 0
hlt : LT.lt (α := ℤ) (↑(padicValNat p n !) : ℤ) (↑n : ℤ)
hnorm : 0 < norm (E := ℚ_[p]) (↑n ! : ℚ_[p])
rw : HMul.hMul (α := ℤ) 1 (↑n : ℤ)
| (↑n : ℤ)

Tactic:
rw [← one_mul (n : ℤ)]

Premises used: Nat.cast, one_mul
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hx0 : ¬x = 0
hlt : LT.lt (α := ℤ) (↑(padicValNat p n !) : ℤ) (↑n : ℤ)
hnorm : 0 < norm (E := ℚ_[p]) (↑n ! : ℚ_[p])
neg : HMul.hMul (α := ℤ) 1 (↑n : ℤ) ≤ HMul.hMul (α := ℤ) (↑x.valuation : ℤ) (↑n : ℤ)
⊢ (↑n : ℤ) ≤ HMul.hMul (α := ℤ) (↑x.valuation : ℤ) (↑n : ℤ)

Tactic:
conv_lhs => rw [← one_mul (n : ℤ)]

Premises used: Nat.cast, one_mul
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hx0 : ¬x = 0
hlt : LT.lt (α := ℤ) (↑(padicValNat p n !) : ℤ) (↑n : ℤ)
hnorm : 0 < norm (E := ℚ_[p]) (↑n ! : ℚ_[p])
neg : LE.le (α := ℤ) 1 (↑x.valuation : ℤ)
⊢ HMul.hMul (α := ℤ) 1 (↑n : ℤ) ≤ HMul.hMul (α := ℤ) (↑x.valuation : ℤ) (↑n : ℤ)

Tactic:
gcongr
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hx0 : ¬x = 0
hlt : LT.lt (α := ℤ) (↑(padicValNat p n !) : ℤ) (↑n : ℤ)
hnorm : 0 < norm (E := ℚ_[p]) (↑n ! : ℚ_[p])
neg : 1 ≤ x.valuation
⊢ LE.le (α := ℤ) 1 (↑x.valuation : ℤ)

Tactic:
norm_cast
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hx0 : ¬x = 0
hlt : LT.lt (α := ℤ) (↑(padicValNat p n !) : ℤ) (↑n : ℤ)
hnorm : 0 < norm (E := ℚ_[p]) (↑n ! : ℚ_[p])
neg : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (β := ℕ) (↑p : ℤ_[p]) 1}) x
neg₁ neg₂ neg₃ neg₄ : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
⊢ 1 ≤ x.valuation

Tactic:
rwa [← PadicInt.mem_span_pow_iff_le_valuation x hx0, pow_one]

Premises used: PadicInt.mem_span_pow_iff_le_valuation, pow_one
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
pos : ∀ (hn : n = 0), ‖(↑n ! : ℚ_[p])⁻¹ʳ * (↑x : ℚ_[p]) ^ n‖ ≤ 1
neg : ∀ (hn : ¬n = 0), ‖(↑n ! : ℚ_[p])⁻¹ʳ * (↑x : ℚ_[p]) ^ n‖ ≤ 1
⊢ ‖(↑n ! : ℚ_[p])⁻¹ʳ * (↑x : ℚ_[p]) ^ n‖ ≤ 1

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hn : n = 0
⊢ ‖(↑n ! : ℚ_[p])⁻¹ʳ * (↑x : ℚ_[p]) ^ n‖ ≤ 1

Tactic:
simp [hn]