awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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
⊢ 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)}))
have 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)}))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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)}))
⊢ 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)}))
have 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)}))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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)}))
⊢ 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)}))
have 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)}))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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)}))
⊢ 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)}))
have 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)}))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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)}))
⊢ 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)}))
have rw₄ : (↑p : O) ∣ x ↔ Membership.mem (γ := Ideal O) (Ideal.span {(↑p : O)}) x
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]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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
⊢ 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)}))
have rw₅ : (↑p : O) ∣ x ↔ (↑p : O) ∣ x
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]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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
⊢ x * y ≠ 0
have 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
Tactic: obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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
⊢ 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
have 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
Tactic: obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (hypothesis)
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
⊢ 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
have h1p : 0 < HDiv.hDiv (α := ℝ) 1 (↑p : ℝ)
Tactic: have h1p : (0 : ℝ) < 1 / p := one_div_pos.2 (Nat.cast_pos.2 hp.1.pos)
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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 : ℝ)
⊢ 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
have 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)
Tactic: rw [← (Ideal.Quotient.mk (Ideal.span {(p : O)})).map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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 : ℝ)
⊢ 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)
have 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)
Tactic: rw [← (Ideal.Quotient.mk (Ideal.span {(p : O)})).map_pow] at hx hy
Cleared hypotheses: hx, s, hy, h1p
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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 : ℝ)
⊢ 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)
have 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)
Tactic: rw [← v_p_lt_val hv] at hx hy ⊢
Cleared hypotheses: hx, s, hy, h1p
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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 : ℝ)
⊢ LT.lt (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0)
    ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) (r * s)) : ℝ≥0)
have 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)
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
Cleared hypotheses: hx, s, hy, h1p
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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 : ℝ)
⊢ LT.lt (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (↑p : K) : ℝ≥0)
    ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) (r * s)) : ℝ≥0)
have 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)
Tactic: rw [map_mul, v.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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)
have 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 : ℝ))
Tactic: refine lt_of_le_of_lt ?_ (mul_lt_mul'' hx hy zero_le' zero_le')