awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Perfection
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
x : O
rw :
  ¬LE.le (α := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) x) : ℝ≥0)
        ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) ↔
    Ne (α := HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
      ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) x :
        HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
      (0 : HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
rw₁ :
  LE.le (α := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) x) : ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) ↔
    Eq (α := HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
      ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) x :
        HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
      (0 : HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
rw₂ :
  LE.le (α := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) x) : ℝ≥0)
      ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) (↑p : O)) : ℝ≥0) ↔
    Eq (α := HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
      ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) x :
        HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
      (0 : HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
rw₃ :
  (↑p : O) ∣ x ↔
    Eq (α := HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
      ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) x :
        HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
      (0 : HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
rw₄ : (↑p : O) ∣ x ↔ Membership.mem (γ := Ideal O) (Ideal.span {(↑p : O)}) x
rw₅ rw₆ : (↑p : O) ∣ x ↔ (↑p : O) ∣ x
⊢ LT.lt (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) x) : ℝ≥0) ↔
    Ne (α := HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
      ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) x :
        HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
      (0 : HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))

Tactic:
rw [lt_iff_not_ge, not_iff_not, ← map_natCast (algebraMap O K) p, hv.le_iff_dvd,
    Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]

Premises used: not_iff_not, lt_iff_not_ge, Algebra.algebraMap, Valuation.Integers.le_iff_dvd, Ideal.Quotient.eq_zero_iff_mem, map_natCast, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Perfection
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
x y : ModP O p
hx : x ^ p ≠ 0
hy : y ^ p ≠ 0
obtain :
  ∀ (r : O)
    (hx :
      HPow.hPow (α := ModP O p)
          ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
            HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
          p ≠
        0),
    HMul.hMul (α := ModP O p)
        ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
          HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
        y ≠
      0
⊢ x * y ≠ 0

Tactic:
obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Perfection
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
y : ModP O p
hy : y ^ p ≠ 0
r : O
hx :
  HPow.hPow (α := ModP O p)
      ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
        HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
      p ≠
    0
obtain :
  ∀ (s : O)
    (hy :
      HPow.hPow (α := ModP O p)
          ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s :
            HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
          p ≠
        0),
    HMul.hMul (α := ModP O p) (β := ModP O p)
        ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
          HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
        ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s :
          HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)})) ≠
      0
⊢ HMul.hMul (α := ModP O p)
      ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
        HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
      y ≠
    0

Tactic:
obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective y

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Perfection
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx :
  HPow.hPow (α := ModP O p)
      ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
        HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
      p ≠
    0
s : O
hy :
  HPow.hPow (α := ModP O p)
      ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s :
        HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
      p ≠
    0
⊢ 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)

Tactic:
have h1p : (0 : ℝ) < 1 / p := one_div_pos.2 (Nat.cast_pos.2 hp.1.pos)
-- Module: Mathlib.RingTheory.Perfection
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx :
  HPow.hPow (α := ModP O p)
      ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
        HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
      p ≠
    0
s : O
hy :
  HPow.hPow (α := ModP O p)
      ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s :
        HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
      p ≠
    0
h1p : 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
rw :
  Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r * s) :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
⊢ HMul.hMul (α := ModP O p) (β := ModP O p)
      ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
        HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
      ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s :
        HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)})) ≠
    0

Tactic:
rw [← (Ideal.Quotient.mk (Ideal.span {(p : O)})).map_mul]

Premises used: Ideal.Quotient.mk, Nat.cast, Ideal.span, RingHom.map_mul, Singleton.singleton
-- Module: Mathlib.RingTheory.Perfection
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx :
  HPow.hPow (α := ModP O p)
      ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r :
        HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
      p ≠
    0
s : O
hy :
  HPow.hPow (α := ModP O p)
      ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s :
        HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
      p ≠
    0
h1p : 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
rw :
  ∀
    (hx :
      Ne (α := ModP O p)
        ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r ^ p) :
          HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
        (0 : ModP O p))
    (s : O)
    (hy :
      Ne (α := ModP O p)
        ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (s ^ p) :
          HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
        (0 : ModP O p))
    (h1p : 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)),
    Ne (α := ModP O p)
      ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r * s) :
        HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
      (0 : ModP O p)
⊢ Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r * s) :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)

Tactic:
rw [← (Ideal.Quotient.mk (Ideal.span {(p : O)})).map_pow] at hx hy

Premises used: Ideal.Quotient.mk, Nat.cast, Ideal.span, Singleton.singleton, RingHom.map_pow
-- Module: Mathlib.RingTheory.Perfection
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx :
  Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r ^ p) :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
s : O
hy :
  Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (s ^ p) :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)
h1p : 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
rw :
  ∀
    (hx :
      LT.lt (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0)
        ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) (r ^ p)) : ℝ≥0))
    (s : O)
    (hy :
      LT.lt (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0)
        ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) (s ^ p)) : ℝ≥0))
    (h1p : 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)),
    LT.lt (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0)
      ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) (r * s)) : ℝ≥0)
⊢ Ne (α := ModP O p)
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r * s) :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : ModP O p)

Tactic:
rw [← v_p_lt_val hv] at hx hy ⊢

Premises used: ModP.v_p_lt_val
-- Module: Mathlib.RingTheory.Perfection
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx :
  LT.lt (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0)
    ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) (r ^ p)) : ℝ≥0)
s : O
hy :
  LT.lt (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0)
    ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) (s ^ p)) : ℝ≥0)
h1p : 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
rw :
  ∀
    (hx :
      HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
        (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r))
    (s : O)
    (hy :
      HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
        (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s))
    (h1p : 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)),
    LT.lt (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0)
      ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) (r * s)) : ℝ≥0)
⊢ LT.lt (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0)
    ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) (r * s)) : ℝ≥0)

Tactic:
rw [map_pow, v.map_pow, ← rpow_lt_rpow_iff h1p, ← rpow_natCast, ← rpow_mul,
    mul_one_div_cancel (Nat.cast_ne_zero.2 hp.1.ne_zero : (p : ℝ) ≠ 0), rpow_one] at hx hy

Premises used: Iff.mpr, NNReal.rpow_natCast, NNReal.rpow_mul, map_pow, NNReal.rpow_lt_rpow_iff, mul_one_div_cancel, Nat.Prime.ne_zero, Valuation.map_pow, NNReal.rpow_one, Fact.out, Nat.cast_ne_zero
-- Module: Mathlib.RingTheory.Perfection
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r)
s : O
hy :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s)
h1p : 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
rw :
  (v : (a : K) → ℝ≥0) (↑p : K) <
    HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r) : ℝ≥0)
      ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s) : ℝ≥0)
⊢ LT.lt (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0)
    ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) (r * s)) : ℝ≥0)

Tactic:
rw [map_mul, v.map_mul]

Premises used: Valuation.map_mul, map_mul
-- Module: Mathlib.RingTheory.Perfection
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r)
s : O
hy :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s)
h1p : 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
⊢ (v : (a : K) → ℝ≥0) (↑p : K) <
    HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r) : ℝ≥0)
      ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s) : ℝ≥0)

Tactic:
lt_of_le_of_lt ?_ (mul_lt_mul'' hx hy zero_le' zero_le')

Premises used: lt_of_le_of_lt, mul_lt_mul'', zero_le'
-- Module: Mathlib.RingTheory.Perfection
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r)
s : O
hy :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s)
h1p : 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
refine :
  (v : (a : K) → ℝ≥0) (↑p : K) ≤
    HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) *
      HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))
⊢ (v : (a : K) → ℝ≥0) (↑p : K) <
    HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r) : ℝ≥0)
      ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s) : ℝ≥0)

Tactic:
refine lt_of_le_of_lt ?_ (mul_lt_mul'' hx hy zero_le' zero_le')

Premises used: lt_of_le_of_lt, mul_lt_mul'', zero_le'
-- Module: Mathlib.RingTheory.Perfection
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r)
s : O
hy :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s)
h1p : 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
pos :
  ∀ (hvp : Eq (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (0 : ℝ≥0)),
    (v : (a : K) → ℝ≥0) (↑p : K) ≤
      HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) *
        HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))
neg :
  ∀ (hvp : ¬Eq (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (0 : ℝ≥0)),
    (v : (a : K) → ℝ≥0) (↑p : K) ≤
      HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) *
        HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))
⊢ (v : (a : K) → ℝ≥0) (↑p : K) ≤
    HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) *
      HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))

Tactic:
by_cases hvp : v p = 0

Premises used: Nat.cast, DFunLike.coe
-- Module: Mathlib.RingTheory.Perfection
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r)
s : O
hy :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s)
h1p : 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
hvp : Eq (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (0 : ℝ≥0)
pos :
  0 ≤ HPow.hPow (α := ℝ≥0) 0 (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) * HPow.hPow (α := ℝ≥0) 0 (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))
⊢ (v : (a : K) → ℝ≥0) (↑p : K) ≤
    HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) *
      HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))

Tactic:
rw [hvp]
-- Module: Mathlib.RingTheory.Perfection
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r)
s : O
hy :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s)
h1p : 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
hvp : Eq (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (0 : ℝ≥0)
⊢ 0 ≤ HPow.hPow (α := ℝ≥0) 0 (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) * HPow.hPow (α := ℝ≥0) 0 (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))

Tactic:
zero_le

Premises used: zero_le
-- Module: Mathlib.RingTheory.Perfection
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r)
s : O
hy :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s)
h1p : 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
hvp : Eq (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (0 : ℝ≥0)
⊢ 0 ≤ HPow.hPow (α := ℝ≥0) 0 (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) * HPow.hPow (α := ℝ≥0) 0 (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))

Tactic:
exact zero_le

Premises used: zero_le
-- Module: Mathlib.RingTheory.Perfection
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r)
s : O
hy :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s)
h1p : 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
hvp : ¬Eq (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (0 : ℝ≥0)
⊢ LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0)

Tactic:
replace hvp := zero_lt_iff.2 hvp
-- Module: Mathlib.RingTheory.Perfection
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r)
s : O
hy :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s)
h1p : 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
hvp : LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0)
rw : HPow.hPow (α := ℝ≥0) (β := ℝ) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) 1
| (v : (a : K) → ℝ≥0) (↑p : K)

Tactic:
rw [← rpow_one (v p)]

Premises used: Nat.cast, NNReal.rpow_one, DFunLike.coe
-- Module: Mathlib.RingTheory.Perfection
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r)
s : O
hy :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s)
h1p : 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
hvp : LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0)
neg :
  HPow.hPow (α := ℝ≥0) (β := ℝ) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) 1 ≤
    HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) *
      HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))
⊢ (v : (a : K) → ℝ≥0) (↑p : K) ≤
    HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) *
      HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))

Tactic:
conv_lhs => rw [← rpow_one (v p)]

Premises used: Nat.cast, NNReal.rpow_one, DFunLike.coe
-- Module: Mathlib.RingTheory.Perfection
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r)
s : O
hy :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s)
h1p : 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
hvp : LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0)
neg :
  HPow.hPow (α := ℝ≥0) (β := ℝ) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) 1 ≤
    HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0)
      (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))
⊢ HPow.hPow (α := ℝ≥0) (β := ℝ) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) 1 ≤
    HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) *
      HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))

Tactic:
rw [← rpow_add (ne_of_gt hvp)]

Premises used: ne_of_gt, NNReal.rpow_add
-- Module: Mathlib.RingTheory.Perfection
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
hp : Fact (Nat.Prime p)
r : O
hx :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) r)
s : O
hy :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)) <
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) s)
h1p : 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
hvp : LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0)
⊢ HPow.hPow (α := ℝ≥0) (β := ℝ) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0) 1 ≤
    HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0)
      (HDiv.hDiv (α := ℝ) 1 (↑p : ℝ) + HDiv.hDiv (α := ℝ) 1 (↑p : ℝ))

Tactic:
rpow_le_rpow_of_exponent_ge hvp (map_natCast (algebraMap O K) p ▸ hv.2 _) ?_

Premises used: Algebra.algebraMap, Valuation.Integers.map_le_one, NNReal.rpow_le_rpow_of_exponent_ge, Eq.rec, map_natCast