awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
pos : x + y = 0 → x = 0 → y = 0 → LE.le (α := WithZero (Multiplicative ℤ)) 0 (max 0 0)
neg : x + y = 0 → x = 0 → ¬y = 0 → 0 ≤ max 0 (exp (-padicValRat p y))
pos₁ : x + y = 0 → ¬x = 0 → y = 0 → 0 ≤ max (exp (-padicValRat p x)) 0
neg₁ : x + y = 0 → ¬x = 0 → ¬y = 0 → 0 ≤ max (exp (-padicValRat p x)) (exp (-padicValRat p y))
pos₂ : ¬x + y = 0 → x = 0 → y = 0 → exp (-padicValRat p (x + y)) ≤ max 0 0
neg₂ : ¬x + y = 0 → x = 0 → ¬y = 0 → exp (-padicValRat p (x + y)) ≤ max 0 (exp (-padicValRat p y))
pos₃ : ¬x + y = 0 → ¬x = 0 → y = 0 → exp (-padicValRat p (x + y)) ≤ max (exp (-padicValRat p x)) 0
neg₃ :
  ¬x + y = 0 → ¬x = 0 → ¬y = 0 → exp (-padicValRat p (x + y)) ≤ max (exp (-padicValRat p x)) (exp (-padicValRat p y))
⊢ (if x + y = 0 then 0 else exp (-padicValRat p (x + y))) ≤
    max (if x = 0 then 0 else exp (-padicValRat p x)) (if y = 0 then 0 else exp (-padicValRat p y))

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
h : x + y = 0
h_1 : x = 0
h_2 : y = 0
⊢ LE.le (α := WithZero (Multiplicative ℤ)) 0 (max 0 0)

Tactic:
simp_all [-exp_neg]

Premises used: WithZero.exp_neg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
h : x + y = 0
h_1 : x = 0
h_2 : ¬y = 0
⊢ 0 ≤ max 0 (exp (-padicValRat p y))

Tactic:
simp_all [-exp_neg]

Premises used: WithZero.exp_neg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
h : x + y = 0
h_1 : ¬x = 0
h_2 : y = 0
⊢ 0 ≤ max (exp (-padicValRat p x)) 0

Tactic:
simp_all [-exp_neg]

Premises used: WithZero.exp_neg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
h : x + y = 0
h_1 : ¬x = 0
h_2 : ¬y = 0
⊢ 0 ≤ max (exp (-padicValRat p x)) (exp (-padicValRat p y))

Tactic:
simp_all [-exp_neg]

Premises used: WithZero.exp_neg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
h : ¬x + y = 0
h_1 : x = 0
h_2 : y = 0
⊢ exp (-padicValRat p (x + y)) ≤ max 0 0

Tactic:
simp_all [-exp_neg]

Premises used: WithZero.exp_neg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
h : ¬x + y = 0
h_1 : x = 0
h_2 : ¬y = 0
⊢ exp (-padicValRat p (x + y)) ≤ max 0 (exp (-padicValRat p y))

Tactic:
simp_all [-exp_neg]

Premises used: WithZero.exp_neg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
h : ¬x + y = 0
h_1 : ¬x = 0
h_2 : y = 0
⊢ exp (-padicValRat p (x + y)) ≤ max (exp (-padicValRat p x)) 0

Tactic:
simp_all [-exp_neg]

Premises used: WithZero.exp_neg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
h : ¬x + y = 0
h_1 : ¬x = 0
h_2 : ¬y = 0
neg : padicValRat p x ≤ padicValRat p (x + y) ∨ padicValRat p y ≤ padicValRat p (x + y)
⊢ exp (-padicValRat p (x + y)) ≤ max (exp (-padicValRat p x)) (exp (-padicValRat p y))

Tactic:
simp_all [-exp_neg]

Premises used: WithZero.exp_neg
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
h : ¬x + y = 0
h_1 : ¬x = 0
h_2 : ¬y = 0
neg : min (padicValRat p x) (padicValRat p y) ≤ padicValRat p (x + y)
⊢ padicValRat p x ≤ padicValRat p (x + y) ∨ padicValRat p y ≤ padicValRat p (x + y)

Tactic:
rw [← min_le_iff]

Premises used: min_le_iff
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
h : ¬x + y = 0
h_1 : ¬x = 0
h_2 : ¬y = 0
⊢ min (padicValRat p x) (padicValRat p y) ≤ padicValRat p (x + y)

Tactic:
padicValRat.min_le_padicValRat_add ‹_›

Premises used: padicValRat.min_le_padicValRat_add
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
h : ¬x + y = 0
h_1 : ¬x = 0
h_2 : ¬y = 0
⊢ min (padicValRat p x) (padicValRat p y) ≤ padicValRat p (x + y)

Tactic:
exact padicValRat.min_le_padicValRat_add ‹_›

Premises used: padicValRat.min_le_padicValRat_add
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℤ
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) (↑x : ℚ) : WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))

Tactic:
rfl

Premises used: Rat.ofInt, rfl, ite
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
⊢ Eq (α := WithZero (Multiplicative ℤ))
      ((padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ)) ↔
    x = 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℤ
⊢ Eq (α := WithZero (Multiplicative ℤ))
      ((padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ)) ↔
    x = 0

Tactic:
simp [← Rat.padicValuation_cast]

Premises used: Rat.padicValuation_cast
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) (↑p : ℚ) : WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))

Tactic:
simp [Rat.padicValuation, Nat.Prime.ne_zero Fact.out]

Premises used: Nat.Prime.ne_zero, Rat.padicValuation, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
⊢ Eq (α := WithZero (Multiplicative ℤ))
    ((padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑p : ℤ) : WithZero (Multiplicative ℤ))
    (exp (-1) : WithZero (Multiplicative ℤ))

Tactic:
simp [← Rat.padicValuation_cast]

Premises used: Rat.padicValuation_cast
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℤ
simp : LE.le (α := WithZero (Multiplicative ℤ)) (if x = 0 then 0 else exp (-(↑(padicValInt p x) : ℤ))) 1
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
simp only [← Rat.padicValuation_cast, Rat.padicValuation, Valuation.coe_mk,
    MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, Rat.intCast_eq_zero_iff, padicValRat.of_int]

Premises used: Rat.padicValuation_cast, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, padicValRat.of_int, Rat.padicValuation, Rat.intCast_eq_zero_iff, Valuation.coe_mk
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℤ
pos : x = 0 → LE.le (α := WithZero (Multiplicative ℤ)) 0 1
neg : ¬x = 0 → LE.le (α := WithZero (Multiplicative ℤ)) (exp (-(↑(padicValInt p x) : ℤ))) 1
⊢ LE.le (α := WithZero (Multiplicative ℤ)) (if x = 0 then 0 else exp (-(↑(padicValInt p x) : ℤ))) 1

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℤ
h : x = 0
⊢ LE.le (α := WithZero (Multiplicative ℤ)) 0 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℤ
h : ¬x = 0
neg : LE.le (α := ℤ) (-(↑(padicValInt p x) : ℤ)) (log 1)
neg₁ : Ne (α := WithZero (Multiplicative ℤ)) 1 0
⊢ LE.le (α := WithZero (Multiplicative ℤ)) (exp (-(↑(padicValInt p x) : ℤ))) 1

Tactic:
rw [← le_log_iff_exp_le]

Premises used: WithZero.le_log_iff_exp_le
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℤ
h : ¬x = 0
⊢ LE.le (α := ℤ) (-(↑(padicValInt p x) : ℤ)) (log 1)

Tactic:
simp_all
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℤ
h : ¬x = 0
⊢ Ne (α := WithZero (Multiplicative ℤ)) 1 0

Tactic:
simp_all
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℤ
simp : Eq (α := WithZero (Multiplicative ℤ)) (if x = 0 then 0 else exp (-(↑(padicValInt p x) : ℤ))) 1 ↔ ¬(↑p : ℤ) ∣ x
⊢ Eq (α := WithZero (Multiplicative ℤ))
      ((padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    ¬(↑p : ℤ) ∣ x

Tactic:
simp only [← Rat.padicValuation_cast, Rat.padicValuation, Valuation.coe_mk,
    MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, Rat.intCast_eq_zero_iff, padicValRat.of_int]

Premises used: Rat.padicValuation_cast, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, padicValRat.of_int, Rat.padicValuation, Rat.intCast_eq_zero_iff, Valuation.coe_mk
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℤ
pos : x = 0 → (Eq (α := WithZero (Multiplicative ℤ)) 0 1 ↔ ¬(↑p : ℤ) ∣ x)
neg : ¬x = 0 → (Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑(padicValInt p x) : ℤ))) 1 ↔ ¬(↑p : ℤ) ∣ x)
⊢ Eq (α := WithZero (Multiplicative ℤ)) (if x = 0 then 0 else exp (-(↑(padicValInt p x) : ℤ))) 1 ↔ ¬(↑p : ℤ) ∣ x

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℤ
h : x = 0
⊢ Eq (α := WithZero (Multiplicative ℤ)) 0 1 ↔ ¬(↑p : ℤ) ∣ x

Tactic:
simp_all
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℤ
h : ¬x = 0
neg : Eq (α := ℤ) (-(↑(padicValInt p x) : ℤ)) 0 ↔ ¬(↑p : ℤ) ∣ x
⊢ Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑(padicValInt p x) : ℤ))) 1 ↔ ¬(↑p : ℤ) ∣ x

Tactic:
rw [← exp_zero, exp_injective.eq_iff]

Premises used: Function.Injective.eq_iff, WithZero.exp_zero, WithZero.exp_injective
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℤ
h : ¬x = 0
⊢ Eq (α := ℤ) (-(↑(padicValInt p x) : ℤ)) 0 ↔ ¬(↑p : ℤ) ∣ x

Tactic:
simp_all [Nat.Prime.ne_one Fact.out]

Premises used: Nat.Prime.ne_one, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℤ
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
      ((padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    (↑p : ℤ) ∣ x

Tactic:
simp [lt_iff_le_and_ne, padicValuation_eq_one_iff, Int.padicValuation_le_one]

Premises used: lt_iff_le_and_ne, Int.padicValuation_eq_one_iff, Int.padicValuation_le_one
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
nth_rw :
  LE.le (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ)) ↔
    Eq (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
nth_rw₁ :
  LT.lt (α := WithZero (Multiplicative ℤ)) (0 : WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      ((padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) x : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)) ↔
    ¬p ∣ x.den

Tactic:
nth_rw 1 [← x.num_div_den, map_div₀, ← Int.natCast_dvd_natCast, ← Int.padicValuation_eq_one_iff,
    Rat.padicValuation_cast, ← Int.cast_natCast, Rat.padicValuation_cast, div_le_one₀]

Premises used: Rat.num_div_den, Int.cast_natCast, Rat.padicValuation_cast, Int.padicValuation_eq_one_iff, map_div₀, div_le_one₀, Int.natCast_dvd_natCast
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
inl :
  ∀
    (h :
      Eq (α := WithZero (Multiplicative ℤ))
        ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))),
    LE.le (α := WithZero (Multiplicative ℤ))
        ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
        ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ)) ↔
      Eq (α := WithZero (Multiplicative ℤ))
        ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))
inr :
  ∀
    (h :
      LT.lt (α := WithZero (Multiplicative ℤ))
        ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))),
    LE.le (α := WithZero (Multiplicative ℤ))
        ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
        ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ)) ↔
      Eq (α := WithZero (Multiplicative ℤ))
        ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ)) ↔
    Eq (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))

Tactic:
rcases (Int.padicValuation_le_one p x.den).eq_or_lt with h | h

Premises used: LE.le.eq_or_lt, Rat.den, Nat.cast, Int.padicValuation_le_one
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
h :
  Eq (α := WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ)) ↔
    Eq (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))

Tactic:
simp [h, Int.padicValuation_le_one]

Premises used: Int.padicValuation_le_one
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
h :
  LT.lt (α := WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
inr :
  LT.lt (α := WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ)) ↔
    Eq (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))

Tactic:
simp only [h.ne, iff_false, not_le]

Premises used: not_le, iff_false, LT.lt.ne
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
h :
  LT.lt (α := WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
inr :
  ∀
    (h' :
      Eq (α := WithZero (Multiplicative ℤ))
        ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))),
    LT.lt (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
inr₁ :
  ∀
    (h' :
      LT.lt (α := WithZero (Multiplicative ℤ))
        ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ))),
    LT.lt (α := WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
      ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))

Tactic:
rcases (Int.padicValuation_le_one p x.num).eq_or_lt with h' | h'

Premises used: LE.le.eq_or_lt, Rat.num, Int.padicValuation_le_one
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
h :
  LT.lt (α := WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
h' :
  Eq (α := WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))

Tactic:
simp [h, h']
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
h :
  LT.lt (α := WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
h' :
  LT.lt (α := WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ Dvd.dvd (α := ℤ) (↑p : ℤ) (↑x.den : ℤ)

Tactic:
rw [Int.padicValuation_lt_one_iff] at h h'

Premises used: Int.padicValuation_lt_one_iff
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
h :
  LT.lt (α := WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
h' :
  LT.lt (α := WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
h₁ : Dvd.dvd (α := ℤ) (↑p : ℤ) (↑x.den : ℤ)
⊢ (↑p : ℤ) ∣ x.num

Tactic:
rw [Int.padicValuation_lt_one_iff] at h h'

Premises used: Int.padicValuation_lt_one_iff
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
h : Dvd.dvd (α := ℤ) (↑p : ℤ) (↑x.den : ℤ)
h' : (↑p : ℤ) ∣ x.num
inr : False
⊢ LT.lt (α := WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) x.num : WithZero (Multiplicative ℤ))

Tactic:
exfalso
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
h : Dvd.dvd (α := ℤ) (↑p : ℤ) (↑x.den : ℤ)
h' : (↑p : ℤ) ∣ x.num
⊢ p ∣ x.den

Tactic:
rw [Int.natCast_dvd_natCast] at h

Premises used: Int.natCast_dvd_natCast
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
h : Dvd.dvd (α := ℤ) (↑p : ℤ) (↑x.den : ℤ)
h' : (↑p : ℤ) ∣ x.num
h₁ : p ∣ x.den
⊢ (↑p : ℤ) ∣ x.num

Tactic:
rw [Int.natCast_dvd_natCast] at h

Premises used: Int.natCast_dvd_natCast
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
h : p ∣ x.den
h' : (↑p : ℤ) ∣ x.num
⊢ p ∣ x.num.natAbs

Tactic:
rw [Int.natCast_dvd] at h'

Premises used: Int.natCast_dvd
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
h : p ∣ x.den
h' : p ∣ x.num.natAbs
⊢ False

Tactic:
Nat.not_coprime_of_dvd_of_dvd (Nat.Prime.one_lt Fact.out) h h' x.reduced.symm

Premises used: Nat.Coprime.symm, Rat.reduced, Nat.Prime.one_lt, Nat.not_coprime_of_dvd_of_dvd, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
h : p ∣ x.den
h' : p ∣ x.num.natAbs
⊢ False

Tactic:
exact Nat.not_coprime_of_dvd_of_dvd (Nat.Prime.one_lt Fact.out) h h' x.reduced.symm

Premises used: Nat.Coprime.symm, Rat.reduced, Nat.Prime.one_lt, Nat.not_coprime_of_dvd_of_dvd, Fact.out
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : ℚ
⊢ LT.lt (α := WithZero (Multiplicative ℤ)) (0 : WithZero (Multiplicative ℤ))
    ((Int.padicValuation p : (a : ℤ) → WithZero (Multiplicative ℤ)) (↑x.den : ℤ) : WithZero (Multiplicative ℤ))

Tactic:
simp [zero_lt_iff]

Premises used: zero_lt_iff
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∃ (a : ℚ),
    Eq (α := WithZero (Multiplicative ℤ))
      ((padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
      (0 : WithZero (Multiplicative ℤ))

Tactic:
simp
-- Module: Mathlib.NumberTheory.Padics.PadicNumbers
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
x : Multiplicative ℤ
coe :
  ∀ (x : ℤ),
    ∃ (a : ℚ),
      Eq (α := WithZero (Multiplicative ℤ))
        ((padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) a : WithZero (Multiplicative ℤ))
        ((↑((Multiplicative.ofAdd : (a : ℤ) → Multiplicative ℤ) x) : WithZero (Multiplicative ℤ)) :
          WithZero (Multiplicative ℤ))
⊢ ∃ (a : ℚ), (padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) a = (↑x : WithZero (Multiplicative ℤ))

Tactic:
induction x with | ofAdd x