awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A : Type u_3
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
⊢ hI' = hI
have h_eq : ∀ (n : ℕ) {a : A}, a ∈ I → hI'.dpow n a = hI.dpow n a
Tactic: ext n a
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A : Type u_3
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
h : a ∈ I
⊢ hI'.dpow n a = hI.dpow n a
have pos : ∀ (ha : a ∈ I), hI'.dpow n a = hI.dpow n a
Tactic: by_cases ha : a ∈ I
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A : Type u_3
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
h : a ∈ I
pos : ∀ (ha : a ∈ I), hI'.dpow n a = hI.dpow n a
⊢ hI'.dpow n a = hI.dpow n a
have neg : ∀ (ha : a ∉ I), hI'.dpow n a = hI.dpow n a
Tactic: by_cases ha : a ∈ I
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A : Type u_3
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
h ha : a ∈ I
⊢ hI'.dpow n a = hI.dpow n a
have pos : ∀ s ∈ S, Membership.mem (α := A) I ((RingHom.id A : (a : A) → A) s : A)
Tactic: refine hI.dpow_comp_from_gens hI' (f := RingHom.id A) hS ?_ ?_ a ha
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A : Type u_3
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
h ha : a ∈ I
pos : ∀ s ∈ S, Membership.mem (α := A) I ((RingHom.id A : (a : A) → A) s : A)
⊢ hI'.dpow n a = hI.dpow n a
have pos₁ : ∀ {n : ℕ}, ∀ a ∈ S, (RingHom.id A : (a : A) → A) (hI.dpow n a) = hI'.dpow n ((RingHom.id A : (a : A) → A) a)
Tactic: refine hI.dpow_comp_from_gens hI' (f := RingHom.id A) hS ?_ ?_ a ha
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A : Type u_3
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
h ha : a ∈ I
s : A
hs : s ∈ S
⊢ Membership.mem (α := A) I ((RingHom.id A : (a : A) → A) s : A)
have pos : Membership.mem (γ := Ideal A) (span S) s
Tactic: simp only [RingHom.id_apply, hS]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A : Type u_3
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
h : a ∈ I
ha : a ∉ I
⊢ hI'.dpow n a = hI.dpow n a
have neg : hI'.dpow n a = 0
Tactic: rw [hI.dpow_null ha, hI'.dpow_null ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A : Type u_3
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
n : ℕ
a : A
h : a ∈ I
ha : a ∉ I
neg : hI'.dpow n a = 0
⊢ hI'.dpow n a = hI.dpow n a
have neg₁ : Eq.{u_3 + 1} (α := A) 0 0
Tactic: rw [hI.dpow_null ha, hI'.dpow_null ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (goal)
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)
x : A
hx : x ∈ I
⊢ Eq.{u_1 + 1} (α := A)
    (if hx : x ∈ I then
      Exists.choose (p := fun (a : A) ↦
        ∃ (_ : Ne (α := ℕ) 0 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow 0 ((f : (a : A) → B) x)) ⋯
    else 0)
    1
have simp : hJ.dpow 0 ((f : (a : A) → B) x) = 1
Tactic: simp only [dif_pos hx, ← hf.eq_iff, (Exists.choose_spec (hmem 0 hx)).2, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (goal)
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)
x : A
hx : x ∈ I
⊢ hJ.dpow 0 ((f : (a : A) → B) x) = 1
have rw : Eq.{u_2 + 1} (α := B) 1 1
Tactic: rw [hJ.dpow_zero (hIJ ▸ Ideal.mem_map_of_mem f hx)]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (hypothesis)
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
⊢ 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))
have hxy : x + y ∈ I
Tactic: have hxy : x + y ∈ I := Ideal.add_mem _ hx hy
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (hypothesis)
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
⊢ (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
have hax : a * x ∈ I
Tactic: have hax : a * x ∈ I := Ideal.mul_mem_left _ _ hx
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (goal)
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
⊢ (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)
have simp : (f : (a : A) → B)
    (if hx_1 :
        (if hx : x ∈ I then
            sorry.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)
                (sorry.choose (p := fun (a : A) ↦
                  ∃ (_ : m ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow m ((f : (a : A) → B) x)))))
        sorry
    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)) sorry) :
      B)
Tactic: simp only [dif_pos hx, ← hf.eq_iff, map_mul, map_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (goal)
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
⊢ (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)
have 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)
              (sorry.choose (p := fun (a : A) ↦
                ∃ (_ : m ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow m ((f : (a : A) → B) x)))))
      sorry) =
  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)) sorry) :
      B)
Tactic: rw [dif_pos]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (goal)
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)
⊢ (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)
have hc : (if hx : x ∈ I then
    sorry.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]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (goal)
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
⊢ (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)
have 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)
Tactic: simp only [(Exists.choose_spec (_ : ∃ a, ∃ _, f a = _)).2]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (goal)
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
⊢ (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
have hc : sorry.choose (p := fun (a : A) ↦ ∃ (_ : m ≠ 0 → a ∈ I), (f : (a : A) → B) a = hJ.dpow m ((f : (a : A) → B) x)) ∈ I
Tactic: rw [dif_pos hx]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
hn : n ≠ 0
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
⊢ ‖(↑n ! : ℚ_[p])⁻¹ʳ * (↑x : ℚ_[p]) ^ n‖ ≤ (↑p : ℝ)⁻¹
have pos : ∀ (hx0 : x = 0), ‖(↑n ! : ℚ_[p])⁻¹ʳ * (↑x : ℚ_[p]) ^ n‖ ≤ (↑p : ℝ)⁻¹
Tactic: by_cases hx0 : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (goal)
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 : ℝ)⁻¹
⊢ ‖(↑n ! : ℚ_[p])⁻¹ʳ * (↑x : ℚ_[p]) ^ n‖ ≤ (↑p : ℝ)⁻¹
have neg : ∀ (hx0 : ¬x = 0), ‖(↑n ! : ℚ_[p])⁻¹ʳ * (↑x : ℚ_[p]) ^ n‖ ≤ (↑p : ℝ)⁻¹
Tactic: by_cases hx0 : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (goal)
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])⁻¹ʳ * (↑x : ℚ_[p]) ^ n‖ ≤ (↑p : ℝ)⁻¹
have pos : ‖(↑n ! : ℚ_[p])⁻¹ʳ * HPow.hPow (α := ℚ_[p]) (↑0 : ℚ_[p]) n‖ ≤ (↑p : ℝ)⁻¹
Tactic: rw [hx0]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (hypothesis)
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])⁻¹ʳ * (↑x : ℚ_[p]) ^ n‖ ≤ (↑p : ℝ)⁻¹
have hlt : 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
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (goal)
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])
have simp : ¬n ! = 0
Tactic: simp only [norm_pos_iff, ne_eq, cast_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (hypothesis)
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 ! : ℚ_[p])⁻¹ʳ * (↑x : ℚ_[p]) ^ n‖ ≤ (↑p : ℝ)⁻¹
have hnorm : 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
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (goal)
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])
⊢ ‖(↑n ! : ℚ_[p])⁻¹ʳ * (↑x : ℚ_[p]) ^ n‖ ≤ (↑p : ℝ)⁻¹
have neg : ‖(↑n ! : ℚ_[p])⁻¹ʳ * (↑x : ℚ_[p]) ^ n‖ < HPow.hPow (α := ℝ) (↑p : ℝ) (HAdd.hAdd (α := ℤ) (-(↑1 : ℤ)) 1)
Tactic: rw [← zpow_neg_one, ← Nat.cast_one (R := ℤ), Padic.norm_le_pow_iff_norm_lt_pow_add_one]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (goal)
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])
⊢ ‖(↑n ! : ℚ_[p])⁻¹ʳ * (↑x : ℚ_[p]) ^ n‖ < HPow.hPow (α := ℝ) (↑p : ℝ) (HAdd.hAdd (α := ℤ) (-(↑1 : ℤ)) 1)
have neg : (norm (E := ℚ_[p]) (↑n ! : ℚ_[p]))⁻¹ * ‖x‖ ^ n < 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]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (goal)
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])
⊢ (norm (E := ℚ_[p]) (↑n ! : ℚ_[p]))⁻¹ * ‖x‖ ^ n < 1
have neg : HPow.hPow (α := ℝ) (↑p : ℝ) (HMul.hMul (α := ℤ) (-(↑x.valuation : ℤ)) (↑n : ℤ)) <
  HPow.hPow (α := ℝ) (↑p : ℝ) (-Padic.valuation (p := p) (↑n ! : ℚ_[p]))
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]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (goal)
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])
⊢ HPow.hPow (α := ℝ) (↑p : ℝ) (HMul.hMul (α := ℤ) (-(↑x.valuation : ℤ)) (↑n : ℤ)) <
    HPow.hPow (α := ℝ) (↑p : ℝ) (-Padic.valuation (p := p) (↑n ! : ℚ_[p]))
have neg : LT.lt (α := ℝ) 1 (↑p : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (goal)
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 : ℝ)
⊢ HPow.hPow (α := ℝ) (↑p : ℝ) (HMul.hMul (α := ℤ) (-(↑x.valuation : ℤ)) (↑n : ℤ)) <
    HPow.hPow (α := ℝ) (↑p : ℝ) (-Padic.valuation (p := p) (↑n ! : ℚ_[p]))
have neg₁ : HMul.hMul (α := ℤ) (-(↑x.valuation : ℤ)) (↑n : ℤ) < -Padic.valuation (p := p) (↑n ! : ℚ_[p])
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (goal)
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])
⊢ HMul.hMul (α := ℤ) (-(↑x.valuation : ℤ)) (↑n : ℤ) < -Padic.valuation (p := p) (↑n ! : ℚ_[p])
have neg : (↑(padicValNat p n !) : ℤ) < HMul.hMul (α := ℤ) (↑x.valuation : ℤ) (↑n : ℤ)
Tactic: simp only [neg_mul, Padic.valuation_natCast, neg_lt_neg_iff]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (goal)
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])
⊢ (↑(padicValNat p n !) : ℤ) < HMul.hMul (α := ℤ) (↑x.valuation : ℤ) (↑n : ℤ)
have neg : (↑n : ℤ) ≤ HMul.hMul (α := ℤ) (↑x.valuation : ℤ) (↑n : ℤ)
Tactic: apply lt_of_lt_of_le hlt
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (goal)
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])
| (↑n : ℤ)
have rw : HMul.hMul (α := ℤ) 1 (↑n : ℤ)
Tactic: rw [← one_mul (n : ℤ)]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (goal)
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])
⊢ (↑n : ℤ) ≤ HMul.hMul (α := ℤ) (↑x.valuation : ℤ) (↑n : ℤ)
have neg : HMul.hMul (α := ℤ) 1 (↑n : ℤ) ≤ HMul.hMul (α := ℤ) (↑x.valuation : ℤ) (↑n : ℤ)
Tactic: conv_lhs => rw [← one_mul (n : ℤ)]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (goal)
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])
⊢ HMul.hMul (α := ℤ) 1 (↑n : ℤ) ≤ HMul.hMul (α := ℤ) (↑x.valuation : ℤ) (↑n : ℤ)
have neg : LE.le (α := ℤ) 1 (↑x.valuation : ℤ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (goal)
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])
⊢ LE.le (α := ℤ) 1 (↑x.valuation : ℤ)
have neg : 1 ≤ x.valuation
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (goal)
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])
⊢ 1 ≤ x.valuation
have neg : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (β := ℕ) (↑p : ℤ_[p]) 1}) x
Tactic: rwa [← PadicInt.mem_span_pow_iff_le_valuation x hx0, pow_one]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Padic (goal)
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
⊢ ‖(↑n ! : ℚ_[p])⁻¹ʳ * (↑x : ℚ_[p]) ^ n‖ ≤ 1
have pos : ∀ (hn : n = 0), ‖(↑n ! : ℚ_[p])⁻¹ʳ * (↑x : ℚ_[p]) ^ n‖ ≤ 1
Tactic: by_cases hn : n = 0