awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
neg : LE.le (α := ℝ) (↑p : ℝ)⁻¹ 1
⊢ ‖(↑n ! : ℚ_[p])⁻¹ʳ * (↑x : ℚ_[p]) ^ n‖ ≤ 1

Tactic:
apply le_trans (dpow'_norm_le_of_ne_zero p hn hx)

Premises used: _private.0.PadicInt.dpow'_norm_le_of_ne_zero, le_trans
-- 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
neg : HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-1) ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) 0
⊢ LE.le (α := ℝ) (↑p : ℝ)⁻¹ 1

Tactic:
rw [← zpow_neg_one, ← zpow_zero ↑p]

Premises used: zpow_neg_one, zpow_zero
-- 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
neg : LE.le (α := ℝ) 1 (↑p : ℝ)
neg₁ : LE.le (α := ℤ) (-1) 0
⊢ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-1) ≤ HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) 0

Tactic:
gcongr
-- 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
⊢ LE.le (α := ℝ) 1 (↑p : ℝ)

Tactic:
exact_mod_cast Nat.Prime.one_le hp.elim

Premises used: Nat.Prime.one_le, Fact.elim
-- 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
⊢ LE.le (α := ℤ) (-1) 0

Tactic:
norm_num
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hm : n ≠ 0
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
⊢ norm (E := ℤ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯) ≤
      HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑1 : ℤ)) ↔
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (β := ℕ) (↑p : ℤ_[p]) 1})
      (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯)

Tactic:
have hiff := PadicInt.norm_le_pow_iff_mem_span_pow ⟨dpow' p n x, dpow'_int p n hx⟩ 1
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hm : n ≠ 0
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hiff :
  norm (E := ℤ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯) ≤
      HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑1 : ℤ)) ↔
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {HPow.hPow (α := ℤ_[p]) (β := ℕ) (↑p : ℤ_[p]) 1})
      (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯)
⊢ norm (E := ℤ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯) ≤
      HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑1 : ℤ)) ↔
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])})
      (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯)

Tactic:
rw [pow_one] at hiff

Premises used: pow_one
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hm : n ≠ 0
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hiff :
  norm (E := ℤ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯) ≤
      HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑1 : ℤ)) ↔
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])})
      (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯)
rw :
  norm (E := ℤ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯) ≤
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑1 : ℤ))
⊢ Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])})
    (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯)

Tactic:
rw [← hiff]
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hm : n ≠ 0
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hiff :
  norm (E := ℤ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯) ≤
      HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑1 : ℤ)) ↔
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])})
      (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯)
simp : norm (E := ℤ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯) ≤ (↑p : ℝ)⁻¹
⊢ norm (E := ℤ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯) ≤
    HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑1 : ℤ))

Tactic:
simp only [cast_one, zpow_neg_one]

Premises used: zpow_neg_one, Nat.cast_one
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hm : n ≠ 0
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hiff :
  norm (E := ℤ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯) ≤
      HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑1 : ℤ)) ↔
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])})
      (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯)
⊢ norm (E := ℤ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯) ≤ (↑p : ℝ)⁻¹

Tactic:
dpow'_norm_le_of_ne_zero p hm hx

Premises used: _private.0.PadicInt.dpow', _private.0.PadicInt.dpow'_norm_le_of_ne_zero
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hm : n ≠ 0
hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
hiff :
  norm (E := ℤ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯) ≤
      HPow.hPow (α := ℝ) (β := ℤ) (↑p : ℝ) (-(↑1 : ℤ)) ↔
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])})
      (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯)
⊢ norm (E := ℤ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯) ≤ (↑p : ℝ)⁻¹

Tactic:
exact dpow'_norm_le_of_ne_zero p hm hx

Premises used: _private.0.PadicInt.dpow'_norm_le_of_ne_zero
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
refine_1 :
  Eq (α := Ideal ℚ_[p]) (Ideal.map (R := ℤ_[p]) (F := ℤ_[p] →+* ℚ_[p]) Coe.ringHom (Ideal.span {(↑p : ℤ_[p])})) ⊤
refine_2 :
  ∀ (n : ℕ) {x : ℤ_[p]},
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x →
      ∃ (y : ℤ_[p]) (_ : n ≠ 0 → Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) y),
        Eq (α := ℚ_[p]) ((Coe.ringHom : (a : ℤ_[p]) → ℚ_[p]) y : ℚ_[p])
          (DividedPowers.dpow (I := ⊤) (RatAlgebra.dividedPowers ⊤) n ((Coe.ringHom : (a : ℤ_[p]) → ℚ_[p]) x) : ℚ_[p])
⊢ DividedPowers (A := ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])})

Tactic:
refine ofInjective (Ideal.span {(p : ℤ_[p])}) (⊤)
    PadicInt.Coe.ringHom ((Set.injective_codRestrict Subtype.property).mp fun ⦃a₁ a₂⦄ a ↦ a)
    (RatAlgebra.dividedPowers (⊤ : Ideal ℚ_[p])) ?_ ?_

Premises used: PadicInt.Coe.ringHom, Set.injective_codRestrict, Nat.cast, DividedPowers.RatAlgebra.dividedPowers, Iff.mp, Ideal.span, DividedPowers.ofInjective, Top.top, Singleton.singleton, Subtype.property
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
refine_1 : Eq (α := Ideal ℚ_[p]) (Ideal.span {(↑p : ℚ_[p])}) ⊤
⊢ Eq (α := Ideal ℚ_[p]) (Ideal.map (R := ℤ_[p]) (F := ℤ_[p] →+* ℚ_[p]) Coe.ringHom (Ideal.span {(↑p : ℤ_[p])})) ⊤

Tactic:
rw [Ideal.map_span, Set.image_singleton, map_natCast]

Premises used: Set.image_singleton, Ideal.map_span, map_natCast
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
refine_1 : ¬p = 0
⊢ Eq (α := Ideal ℚ_[p]) (Ideal.span {(↑p : ℚ_[p])}) ⊤

Tactic:
simp only [Ideal.span_singleton_eq_top, isUnit_iff_ne_zero, ne_eq, cast_eq_zero]

Premises used: Ideal.span_singleton_eq_top, isUnit_iff_ne_zero, ne_eq, Nat.cast_eq_zero
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ¬p = 0

Tactic:
Nat.Prime.ne_zero hp.elim

Premises used: Fact.elim, Nat.Prime.ne_zero
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ¬p = 0

Tactic:
exact Nat.Prime.ne_zero hp.elim

Premises used: Fact.elim, Nat.Prime.ne_zero
-- 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
⊢ Eq (α := ℚ_[p])
    ((Coe.ringHom : (a : ℤ_[p]) → ℚ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯) :
      ℚ_[p])
    (DividedPowers.dpow (I := ⊤) (RatAlgebra.dividedPowers ⊤) n ((Coe.ringHom : (a : ℤ_[p]) → ℚ_[p]) x) : ℚ_[p])

Tactic:
simp [dpow', inverse_eq_inv', Coe.ringHom_apply, RatAlgebra.dpow_apply,
        Submodule.mem_top, ↓reduceIte]

Premises used: Ring.inverse_eq_inv', PadicInt.Coe.ringHom_apply, DividedPowers.RatAlgebra.dpow_apply, _private.0.PadicInt.dpow', reduceIte, Submodule.mem_top
-- 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
⊢ ∃ (y : ℤ_[p]) (_ : n ≠ 0 → Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) y),
    Eq (α := ℚ_[p]) ((Coe.ringHom : (a : ℤ_[p]) → ℚ_[p]) y : ℚ_[p])
      (DividedPowers.dpow (I := ⊤) (RatAlgebra.dividedPowers ⊤) n ((Coe.ringHom : (a : ℤ_[p]) → ℚ_[p]) x) : ℚ_[p])

Tactic:
exact ⟨⟨dpow' p n x, dpow'_int p n hx⟩, fun hn ↦ dpow'_mem p hn hx, by
      simp [dpow', inverse_eq_inv', Coe.ringHom_apply, RatAlgebra.dpow_apply,
        Submodule.mem_top, ↓reduceIte]⟩
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
refine_1 :
  Eq (α := Ideal ℚ_[p]) (Ideal.map (R := ℤ_[p]) (F := ℤ_[p] →+* ℚ_[p]) Coe.ringHom (Ideal.span {(↑p : ℤ_[p])})) ⊤
refine_2 refine_2₁ :
  ∀ (n : ℕ) {x : ℤ_[p]},
    Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x →
      ∃ (y : ℤ_[p]) (_ : n ≠ 0 → Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) y),
        Eq (α := ℚ_[p]) ((Coe.ringHom : (a : ℤ_[p]) → ℚ_[p]) y : ℚ_[p])
          (DividedPowers.dpow (I := ⊤) (RatAlgebra.dividedPowers ⊤) n ((Coe.ringHom : (a : ℤ_[p]) → ℚ_[p]) x) : ℚ_[p])
⊢ DividedPowers (A := ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])})

Tactic:
classical
  refine ofInjective (Ideal.span {(p : ℤ_[p])}) (⊤)
    PadicInt.Coe.ringHom ((Set.injective_codRestrict Subtype.property).mp fun ⦃a₁ a₂⦄ a ↦ a)
    (RatAlgebra.dividedPowers (⊤ : Ideal ℚ_[p])) ?_ ?_
  · rw [Ideal.map_span, Set.image_singleton, map_natCast]
    simp only [Ideal.span_singleton_eq_top, isUnit_iff_ne_zero, ne_eq, cast_eq_zero]
    exact Nat.Prime.ne_zero hp.elim
  · intro n x hx
    exact ⟨⟨dpow' p n x, dpow'_int p n hx⟩, fun hn ↦ dpow'_mem p hn hx, by
      simp [dpow', inverse_eq_inv', Coe.ringHom_apply, RatAlgebra.dpow_apply,
        Submodule.mem_top, ↓reduceIte]⟩

Premises used: Set.image_singleton, Ideal.map_span, Ideal.span_singleton_eq_top, isUnit_iff_ne_zero, ne_eq, map_natCast, Nat.cast_eq_zero, Fact.elim, Nat.Prime.ne_zero
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
pos :
  ∀ (hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x),
    Eq (α := ℤ_[p])
      (Exists.choose (p := fun (a : ℤ_[p]) ↦
        ∃ (_ : n ≠ 0 → Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) a),
          Eq (α := ℚ_[p]) ((Coe.ringHom : (a : ℤ_[p]) → ℚ_[p]) a : ℚ_[p])
            (DividedPowers.dpow (I := ⊤) (RatAlgebra.dividedPowers ⊤) n ((Coe.ringHom : (a : ℤ_[p]) → ℚ_[p]) x) :
              ℚ_[p]))
        ⋯)
      (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯)
neg : ∀ (hx : x ∉ Ideal.span {(↑p : ℤ_[p])}), Eq (α := ℤ_[p]) 0 0
⊢ Eq (α := ℤ_[p])
    (if hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x then
      Exists.choose (p := fun (a : ℤ_[p]) ↦
        ∃ (_ : n ≠ 0 → Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) a),
          Eq (α := ℚ_[p]) ((Coe.ringHom : (a : ℤ_[p]) → ℚ_[p]) a : ℚ_[p])
            (DividedPowers.dpow (I := ⊤) (RatAlgebra.dividedPowers ⊤) n ((Coe.ringHom : (a : ℤ_[p]) → ℚ_[p]) x) :
              ℚ_[p]))
        ⋯
    else 0)
    (if hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x then
      Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯
    else 0)

Tactic:
split_ifs with hx
-- 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
⊢ Injective (α := ℤ_[p]) (β := ℚ_[p]) (⇑Coe.ringHom : (a : ℤ_[p]) → ℚ_[p])

Tactic:
have hinj : Injective (PadicInt.Coe.ringHom (p := p)) :=
      (Set.injective_codRestrict Subtype.property).mp fun ⦃a₁ a₂⦄ a ↦ a
-- 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
hinj : Injective (α := ℤ_[p]) (β := ℚ_[p]) (⇑Coe.ringHom : (a : ℤ_[p]) → ℚ_[p])
⊢ (Coe.ringHom : (a : ℤ_[p]) → ℚ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯) =
    (↑n ! : ℚ_[p])⁻¹ʳ * HPow.hPow (α := ℚ_[p]) ((Coe.ringHom : (a : ℤ_[p]) → ℚ_[p]) x : ℚ_[p]) n

Tactic:
simp [dpow', inverse_eq_inv', Coe.ringHom_apply]

Premises used: Ring.inverse_eq_inv', PadicInt.Coe.ringHom_apply, _private.0.PadicInt.dpow'
-- 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
hinj : Injective (α := ℤ_[p]) (β := ℚ_[p]) (⇑Coe.ringHom : (a : ℤ_[p]) → ℚ_[p])
⊢ (Coe.ringHom : (a : ℤ_[p]) → ℚ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯) =
    (↑n ! : ℚ_[p])⁻¹ʳ * HPow.hPow (α := ℚ_[p]) ((Coe.ringHom : (a : ℤ_[p]) → ℚ_[p]) x : ℚ_[p]) n

Tactic:
have heq : Coe.ringHom ⟨dpow' p n x, dpow'_int p n hx⟩ =
        inverse (n ! : ℚ_[p]) * Coe.ringHom x ^ n := by
      simp [dpow', inverse_eq_inv', Coe.ringHom_apply]
-- 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
hinj : Injective (α := ℤ_[p]) (β := ℚ_[p]) (⇑Coe.ringHom : (a : ℤ_[p]) → ℚ_[p])
heq :
  (Coe.ringHom : (a : ℤ_[p]) → ℚ_[p]) (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯) =
    (↑n ! : ℚ_[p])⁻¹ʳ * HPow.hPow (α := ℚ_[p]) ((Coe.ringHom : (a : ℤ_[p]) → ℚ_[p]) x : ℚ_[p]) n
⊢ Eq (α := ℤ_[p])
    (Exists.choose (p := fun (a : ℤ_[p]) ↦
      ∃ (_ : n ≠ 0 → Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) a),
        Eq (α := ℚ_[p]) ((Coe.ringHom : (a : ℤ_[p]) → ℚ_[p]) a : ℚ_[p])
          (DividedPowers.dpow (I := ⊤) (RatAlgebra.dividedPowers ⊤) n ((Coe.ringHom : (a : ℤ_[p]) → ℚ_[p]) x) : ℚ_[p]))
      ⋯)
    (Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) (dpow' p n (↑x : ℚ_[p])) ⋯)

Tactic:
simpa only [← hinj.eq_iff, (Exists.choose_spec (_ : ∃ a, ∃ _, Coe.ringHom a = _)).2,
      RatAlgebra.dpow_apply, Submodule.mem_top] using heq.symm

Premises used: Exists.choose_spec, Function.Injective.eq_iff, DividedPowers.RatAlgebra.dpow_apply, Eq.symm, Submodule.mem_top
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∉ Ideal.span {(↑p : ℤ_[p])}
⊢ Eq (α := ℤ_[p]) 0 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
simp :
  (↑(if hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x then
          Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) ((↑n ! : ℚ_[p])⁻¹ * (↑x : ℚ_[p]) ^ n) ⋯
        else 0) :
      ℚ_[p]) =
    if Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x then (↑n ! : ℚ_[p])⁻¹ * (↑x : ℚ_[p]) ^ n else 0
⊢ (↑(DividedPowers.dpow (dividedPowers p) n x) : ℚ_[p]) =
    if x_1 : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x then (↑n ! : ℚ_[p])⁻¹ʳ * (↑x : ℚ_[p]) ^ n
    else 0

Tactic:
simp only [dividedPowers_eq, dpow', inverse_eq_inv', dite_eq_ite]

Premises used: Ring.inverse_eq_inv', _private.0.PadicInt.dividedPowers_eq, _private.0.PadicInt.dpow', dite_eq_ite
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
pos :
  ∀ (h : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x),
    (↑(Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) ((↑n ! : ℚ_[p])⁻¹ * (↑x : ℚ_[p]) ^ n) ⋯) : ℚ_[p]) =
      (↑n ! : ℚ_[p])⁻¹ * (↑x : ℚ_[p]) ^ n
neg : x ∉ Ideal.span {(↑p : ℤ_[p])} → Eq (α := ℚ_[p]) (↑0 : ℚ_[p]) 0
⊢ (↑(if hx : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x then
          Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) ((↑n ! : ℚ_[p])⁻¹ * (↑x : ℚ_[p]) ^ n) ⋯
        else 0) :
      ℚ_[p]) =
    if Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x then (↑n ! : ℚ_[p])⁻¹ * (↑x : ℚ_[p]) ^ n else 0

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : Membership.mem (γ := Ideal ℤ_[p]) (Ideal.span {(↑p : ℤ_[p])}) x
⊢ (↑(Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1) ((↑n ! : ℚ_[p])⁻¹ * (↑x : ℚ_[p]) ^ n) ⋯) : ℚ_[p]) =
    (↑n ! : ℚ_[p])⁻¹ * (↑x : ℚ_[p]) ^ n

Tactic:
simp
-- Module: Mathlib.RingTheory.DividedPowers.Padic
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : x ∉ Ideal.span {(↑p : ℤ_[p])}
⊢ Eq (α := ℚ_[p]) (↑0 : ℚ_[p]) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
m : ℕ
x : A
hx : x ∈ I
⊢ dpow I m x = (↑m ! : A)⁻¹ʳ * x ^ m

Tactic:
simp [dpow, hx]

Premises used: DividedPowers.OfInvertibleFactorial.dpow
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
m : ℕ
x : A
hx : x ∉ I
⊢ dpow I m x = 0

Tactic:
simp [dpow, hx]

Premises used: DividedPowers.OfInvertibleFactorial.dpow
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
x : A
hx : x ∈ I
⊢ dpow I 0 x = 1

Tactic:
simp [dpow, hx]

Premises used: DividedPowers.OfInvertibleFactorial.dpow
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
x : A
hx : x ∈ I
⊢ dpow I 1 x = x

Tactic:
simp [dpow_eq_of_mem hx]

Premises used: DividedPowers.OfInvertibleFactorial.dpow_eq_of_mem
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
m : ℕ
hm : m ≠ 0
x : A
hx : x ∈ I
rw : (↑m ! : A)⁻¹ʳ * x ^ m ∈ I
⊢ dpow I m x ∈ I

Tactic:
rw [dpow_eq_of_mem hx]

Premises used: DividedPowers.OfInvertibleFactorial.dpow_eq_of_mem
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
m : ℕ
hm : m ≠ 0
x : A
hx : x ∈ I
⊢ (↑m ! : A)⁻¹ʳ * x ^ m ∈ I

Tactic:
Ideal.mul_mem_left I _ (Ideal.pow_mem_of_mem I hx _ (Nat.pos_of_ne_zero hm))

Premises used: Ideal.pow_mem_of_mem, Nat.pos_of_ne_zero, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
m : ℕ
hm : m ≠ 0
x : A
hx : x ∈ I
⊢ (↑m ! : A)⁻¹ʳ * x ^ m ∈ I

Tactic:
exact Ideal.mul_mem_left I _ (Ideal.pow_mem_of_mem I hx _ (Nat.pos_of_ne_zero hm))

Premises used: Ideal.pow_mem_of_mem, Nat.pos_of_ne_zero, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
rw : (↑m ! : A)⁻¹ʳ * (x + y) ^ m = ∑ k ∈ @Finset.antidiagonal _ instAddMonoid _ m, dpow I k.1 x * dpow I k.2 y
⊢ dpow I m (x + y) = ∑ k ∈ @Finset.antidiagonal _ instAddMonoid _ m, dpow I k.1 x * dpow I k.2 y

Tactic:
rw [dpow_eq_of_mem (Ideal.add_mem I hx hy)]

Premises used: Ideal.add_mem, DividedPowers.OfInvertibleFactorial.dpow_eq_of_mem
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
simp :
  (↑m ! : A)⁻¹ʳ * (x + y) ^ m =
    ∑ x_1 ∈ @Finset.antidiagonal _ instAddMonoid _ m,
      (if x ∈ I then (↑x_1.1! : A)⁻¹ʳ * x ^ x_1.1 else 0) * if y ∈ I then (↑x_1.2! : A)⁻¹ʳ * y ^ x_1.2 else 0
⊢ (↑m ! : A)⁻¹ʳ * (x + y) ^ m = ∑ k ∈ @Finset.antidiagonal _ instAddMonoid _ m, dpow I k.1 x * dpow I k.2 y

Tactic:
simp only [dpow]

Premises used: DividedPowers.OfInvertibleFactorial.dpow
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
rw :
  Eq.{u_1 + 1} (α := A) (∑ m_1 ∈ @Finset.antidiagonal _ instAddMonoid _ m, m.choose m_1.1 • (x ^ m_1.1 * y ^ m_1.2))
    (∑ i ∈ @Finset.antidiagonal _ instAddMonoid _ m,
      (↑m ! : A) * ((if x ∈ I then (↑i.1! : A)⁻¹ʳ * x ^ i.1 else 0) * if y ∈ I then (↑i.2! : A)⁻¹ʳ * y ^ i.2 else 0))
⊢ (↑m ! : A)⁻¹ʳ * (x + y) ^ m =
    ∑ x_1 ∈ @Finset.antidiagonal _ instAddMonoid _ m,
      (if x ∈ I then (↑x_1.1! : A)⁻¹ʳ * x ^ x_1.1 else 0) * if y ∈ I then (↑x_1.2! : A)⁻¹ʳ * y ^ x_1.2 else 0

Tactic:
rw [inverse_mul_eq_iff_eq_mul _ _ _ (hn_fac.natCast_factorial_of_lt hmn),
    Finset.mul_sum, Commute.add_pow' (Commute.all _ _)]

Premises used: Finset.mul_sum, Ring.inverse_mul_eq_iff_eq_mul, IsUnit.natCast_factorial_of_lt, Commute.add_pow'
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
apply :
  ∀ x_1 ∈ @Finset.antidiagonal _ instAddMonoid _ m,
    m.choose x_1.1 • (x ^ x_1.1 * y ^ x_1.2) =
      (↑m ! : A) *
        ((if x ∈ I then (↑x_1.1! : A)⁻¹ʳ * x ^ x_1.1 else 0) * if y ∈ I then (↑x_1.2! : A)⁻¹ʳ * y ^ x_1.2 else 0)
⊢ Eq.{u_1 + 1} (α := A) (∑ m_1 ∈ @Finset.antidiagonal _ instAddMonoid _ m, m.choose m_1.1 • (x ^ m_1.1 * y ^ m_1.2))
    (∑ i ∈ @Finset.antidiagonal _ instAddMonoid _ m,
      (↑m ! : A) * ((if x ∈ I then (↑i.1! : A)⁻¹ʳ * x ^ i.1 else 0) * if y ∈ I then (↑i.2! : A)⁻¹ʳ * y ^ i.2 else 0))

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ @Finset.antidiagonal _ instAddMonoid _ m
rw : m.choose k.1 • (x ^ k.1 * y ^ k.2) = (↑m ! : A) * ((↑k.1! : A)⁻¹ʳ * x ^ k.1 * ((↑k.2! : A)⁻¹ʳ * y ^ k.2))
⊢ m.choose k.1 • (x ^ k.1 * y ^ k.2) =
    (↑m ! : A) * ((if x ∈ I then (↑k.1! : A)⁻¹ʳ * x ^ k.1 else 0) * if y ∈ I then (↑k.2! : A)⁻¹ʳ * y ^ k.2 else 0)

Tactic:
rw [if_pos hx, if_pos hy]

Premises used: if_pos
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
m : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ @Finset.antidiagonal _ instAddMonoid _ m
ring_nf : x ^ k.1 * y ^ k.2 * (↑(m.choose k.1) : A) = x ^ k.1 * y ^ k.2 * (↑m ! : A) * (↑k.1! : A)⁻¹ʳ * (↑k.2! : A)⁻¹ʳ
⊢ m.choose k.1 • (x ^ k.1 * y ^ k.2) = (↑m ! : A) * ((↑k.1! : A)⁻¹ʳ * x ^ k.1 * ((↑k.2! : A)⁻¹ʳ * y ^ k.2))

Tactic:
ring_nf