awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R_1 p
R : Type u₁
inst_2 : CommSemiring R
inst_3 : CharP R p
inst_4 : PerfectRing R p
S : Type u₂
inst_5 : CommSemiring S
inst_6 : CharP S p
f : RingHom.{u₁, u₂} R (Perfection S p)
r : R
n : ℕ
rw :
  Eq (α := S)
    ((coeff S p (0 + n) : (a : Perfection S p) → S)
        ((⇑(frobenius (Perfection S p) p) : (a : Perfection S p) → Perfection S p)^[n]
            ((f : (a : R) → Perfection S p) ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] r)) :
          Perfection S p) :
      S)
    ((coeff S p n : (a : Perfection S p) → S) ((f : (a : R) → Perfection S p) r : Perfection S p) : S)
⊢ Eq (α := S)
    ((coeff S p 0 : (a : Perfection S p) → S)
        ((f : (a : R) → Perfection S p) ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] r) :
          Perfection S p) :
      S)
    ((coeff S p n : (a : Perfection S p) → S) ((f : (a : R) → Perfection S p) r : Perfection S p) : S)
have rw₁ : Eq (α := S)
  ((coeff S p n : (a : Perfection S p) → S)
      ((⇑(frobenius (Perfection S p) p) : (a : Perfection S p) → Perfection S p)^[n]
          ((f : (a : R) → Perfection S p) ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] r)) :
        Perfection S p) :
    S)
  ((coeff S p n : (a : Perfection S p) → S) ((f : (a : R) → Perfection S p) r : Perfection S p) : S)
Tactic: rw [← coeff_iterate_frobenius _ 0 n, zero_add, ← RingHom.map_iterate_frobenius,
        Function.RightInverse.iterate (frobenius_apply_frobeniusEquiv_symm R p) n]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R_1 p
R : Type u₁
inst_2 : CommSemiring R
inst_3 : CharP R p
inst_4 : PerfectRing R p
S : Type u₂
inst_5 : CommSemiring S
inst_6 : CharP S p
f : RingHom.{u₁, u₂} R (Perfection S p)
r : R
n : ℕ
rw :
  Eq (α := S)
    ((coeff S p (0 + n) : (a : Perfection S p) → S)
        ((⇑(frobenius (Perfection S p) p) : (a : Perfection S p) → Perfection S p)^[n]
            ((f : (a : R) → Perfection S p) ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] r)) :
          Perfection S p) :
      S)
    ((coeff S p n : (a : Perfection S p) → S) ((f : (a : R) → Perfection S p) r : Perfection S p) : S)
rw₁ :
  Eq (α := S)
    ((coeff S p n : (a : Perfection S p) → S)
        ((⇑(frobenius (Perfection S p) p) : (a : Perfection S p) → Perfection S p)^[n]
            ((f : (a : R) → Perfection S p) ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] r)) :
          Perfection S p) :
      S)
    ((coeff S p n : (a : Perfection S p) → S) ((f : (a : R) → Perfection S p) r : Perfection S p) : S)
⊢ Eq (α := S)
    ((coeff S p 0 : (a : Perfection S p) → S)
        ((f : (a : R) → Perfection S p) ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] r) :
          Perfection S p) :
      S)
    ((coeff S p n : (a : Perfection S p) → S) ((f : (a : R) → Perfection S p) r : Perfection S p) : S)
have rw₂ : Eq (α := S)
  ((coeff S p n : (a : Perfection S p) → S)
      ((f : (a : R) → Perfection S p)
          ((⇑(frobenius R p) : (a : R) → R)^[n] ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] r)) :
        Perfection S p) :
    S)
  ((coeff S p n : (a : Perfection S p) → S) ((f : (a : R) → Perfection S p) r : Perfection S p) : S)
Tactic: rw [← coeff_iterate_frobenius _ 0 n, zero_add, ← RingHom.map_iterate_frobenius,
        Function.RightInverse.iterate (frobenius_apply_frobeniusEquiv_symm R p) n]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : CharP R_1 p
R : Type u₁
inst_2 : CommSemiring R
inst_3 : CharP R p
inst_4 : PerfectRing R p
S : Type u₂
inst_5 : CommSemiring S
inst_6 : CharP S p
f : RingHom.{u₁, u₂} R (Perfection S p)
r : R
n : ℕ
rw :
  Eq (α := S)
    ((coeff S p (0 + n) : (a : Perfection S p) → S)
        ((⇑(frobenius (Perfection S p) p) : (a : Perfection S p) → Perfection S p)^[n]
            ((f : (a : R) → Perfection S p) ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] r)) :
          Perfection S p) :
      S)
    ((coeff S p n : (a : Perfection S p) → S) ((f : (a : R) → Perfection S p) r : Perfection S p) : S)
rw₁ :
  Eq (α := S)
    ((coeff S p n : (a : Perfection S p) → S)
        ((⇑(frobenius (Perfection S p) p) : (a : Perfection S p) → Perfection S p)^[n]
            ((f : (a : R) → Perfection S p) ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] r)) :
          Perfection S p) :
      S)
    ((coeff S p n : (a : Perfection S p) → S) ((f : (a : R) → Perfection S p) r : Perfection S p) : S)
rw₂ :
  Eq (α := S)
    ((coeff S p n : (a : Perfection S p) → S)
        ((f : (a : R) → Perfection S p)
            ((⇑(frobenius R p) : (a : R) → R)^[n] ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] r)) :
          Perfection S p) :
      S)
    ((coeff S p n : (a : Perfection S p) → S) ((f : (a : R) → Perfection S p) r : Perfection S p) : S)
⊢ Eq (α := S)
    ((coeff S p 0 : (a : Perfection S p) → S)
        ((f : (a : R) → Perfection S p) ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] r) :
          Perfection S p) :
      S)
    ((coeff S p n : (a : Perfection S p) → S) ((f : (a : R) → Perfection S p) r : Perfection S p) : S)
have rw₃ : Eq (α := S) ((coeff S p n : (a : Perfection S p) → S) ((f : (a : R) → Perfection S p) r : Perfection S p) : S)
  ((coeff S p n : (a : Perfection S p) → S) ((f : (a : R) → Perfection S p) r : Perfection S p) : S)
Tactic: rw [← coeff_iterate_frobenius _ 0 n, zero_add, ← RingHom.map_iterate_frobenius,
        Function.RightInverse.iterate (frobenius_apply_frobeniusEquiv_symm R p) n]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u₁
inst_1 : CommSemiring R
inst_2 : CharP R p
inst_3 : PerfectRing R p
f : ℕ → R
hf : ∀ (n : ℕ), f (n + 1) ^ p = f n
n_1 n : ℕ
ih : (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] (f 0) = f n
⊢ (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n.succ] (f 0) ^ p = f n.succ ^ p
have rw : HPow.hPow (α := R)
    ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R)
        ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] (f 0)) :
      R)
    p =
  f n.succ ^ p
Tactic: rw [Function.iterate_succ_apply', frobeniusEquiv_symm_pow_p, ih, hf]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u₁
inst_1 : CommSemiring R
inst_2 : CharP R p
inst_3 : PerfectRing R p
f : ℕ → R
hf : ∀ (n : ℕ), f (n + 1) ^ p = f n
n_1 n : ℕ
ih : (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] (f 0) = f n
rw :
  HPow.hPow (α := R)
      ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R)
          ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] (f 0)) :
        R)
      p =
    f n.succ ^ p
⊢ (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n.succ] (f 0) ^ p = f n.succ ^ p
have rw₁ : (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] (f 0) = f n.succ ^ p
Tactic: rw [Function.iterate_succ_apply', frobeniusEquiv_symm_pow_p, ih, hf]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u₁
inst_1 : CommSemiring R
inst_2 : CharP R p
inst_3 : PerfectRing R p
f : ℕ → R
hf : ∀ (n : ℕ), f (n + 1) ^ p = f n
n_1 n : ℕ
ih : (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] (f 0) = f n
rw :
  HPow.hPow (α := R)
      ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R)
          ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] (f 0)) :
        R)
      p =
    f n.succ ^ p
rw₁ : (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] (f 0) = f n.succ ^ p
⊢ (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n.succ] (f 0) ^ p = f n.succ ^ p
have rw₂ : f n = f n.succ ^ p
Tactic: rw [Function.iterate_succ_apply', frobeniusEquiv_symm_pow_p, ih, hf]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u₁
inst_1 : CommSemiring R
inst_2 : CharP R p
inst_3 : PerfectRing R p
f : ℕ → R
hf : ∀ (n : ℕ), f (n + 1) ^ p = f n
n_1 n : ℕ
ih : (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] (f 0) = f n
rw :
  HPow.hPow (α := R)
      ((RingEquiv.symm (frobeniusEquiv R p) : (a : R) → R)
          ((⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] (f 0)) :
        R)
      p =
    f n.succ ^ p
rw₁ : (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n] (f 0) = f n.succ ^ p
rw₂ : f n = f n.succ ^ p
⊢ (⇑(RingEquiv.symm (frobeniusEquiv R p)) : (a : R) → R)^[n.succ] (f 0) ^ p = f n.succ ^ p
have rw₃ : f n = f n
Tactic: rw [Function.iterate_succ_apply', frobeniusEquiv_symm_pow_p, ih, hf]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u₁
inst_1 : CommSemiring R
inst_2 : CharP R p
P_1 : Type u₃
inst_3 : CommSemiring P_1
inst_4 : CharP P_1 p
inst_5 : PerfectRing P_1 p
inst_6 : PerfectRing R p
S : Type u₂
inst_7 : CommSemiring S
inst_8 : CharP S p
P : Type u₃
inst_9 : CommSemiring P
inst_10 : CharP P p
inst_11 : PerfectRing P p
π : P →+* S
m : PerfectionMap p π
f : R →+* S
⊢ (fun (f : R →+* P) ↦ π.comp f)
      ((fun (f : R →+* S) ↦
          (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑m.equiv.symm : Perfection S p →+* P)
              ((Perfection.lift p R S : (a : R →+* S) → R →+* Perfection S p) f) :
            R →+* P))
        f) =
    f
have simp_rw : @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (Perfection.coeff S p 0)
    ((Perfection.lift p R S : (a : R →+* S) → R →+* Perfection S p) f) =
  f
Tactic: simp_rw [← RingHom.comp_assoc, comp_symm_equiv']
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u₁
inst_1 : CommSemiring R
inst_2 : CharP R p
P_1 : Type u₃
inst_3 : CommSemiring P_1
inst_4 : CharP P_1 p
inst_5 : PerfectRing P_1 p
inst_6 : PerfectRing R p
S : Type u₂
inst_7 : CommSemiring S
inst_8 : CharP S p
P : Type u₃
inst_9 : CommSemiring P
inst_10 : CharP P p
inst_11 : PerfectRing P p
π : P →+* S
m : PerfectionMap p π
f : R →+* P
x : R
⊢ Eq (α := RingHom.{u₁, u₂} R (Perfection S p))
    ((Perfection.lift p R S : (a : R →+* S) → R →+* Perfection S p) (π.comp f) : RingHom.{u₁, u₂} R (Perfection S p))
    (RingHom.comp (↑m.equiv : P →+* Perfection S p) f : RingHom.{u₁, u₂} R (Perfection S p))
have rw : π.comp f =
  (Equiv.symm (Perfection.lift p R S) : (a : R →+* Perfection S p) → R →+* S)
    (RingHom.comp (↑m.equiv : P →+* Perfection S p) f)
Tactic: rw [Equiv.apply_eq_iff_eq_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u₁
inst_1 : CommSemiring R
inst_2 : CharP R p
S : Type u₂
inst_3 : CommSemiring S
inst_4 : CharP S p
φ : R →+* S
f : Perfection R p
⊢ Eq (α := S)
    ((Perfection.coeff S p 0 : (a : Perfection S p) → S)
        (((map p ⋯ ⋯ φ : RingHom.{u₁, u₂} (Perfection R p) (Perfection S p)) : (a : Perfection R p) → Perfection S p)
            f :
          Perfection S p) :
      S)
    ((Perfection.coeff S p 0 : (a : Perfection S p) → S)
        (((Perfection.map p φ : RingHom.{u₁, u₂} (Perfection R p) (Perfection S p)) :
              (a : Perfection R p) → Perfection S p)
            f :
          Perfection S p) :
      S)
have rw : Eq.{u₂ + 1} (α := S) ((φ : (a : R) → S) ((Perfection.coeff R p 0 : (a : Perfection R p) → R) f : R) : S)
  ((Perfection.coeff S p 0 : (a : Perfection S p) → S)
      (((Perfection.map p φ : RingHom.{u₁, u₂} (Perfection R p) (Perfection S p)) :
            (a : Perfection R p) → Perfection S p)
          f :
        Perfection S p) :
    S)
Tactic: rw [map_map, Perfection.coeff_map]
-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u₁
inst_1 : CommSemiring R
inst_2 : CharP R p
S : Type u₂
inst_3 : CommSemiring S
inst_4 : CharP S p
φ : R →+* S
f : Perfection R p
rw :
  Eq.{u₂ + 1} (α := S) ((φ : (a : R) → S) ((Perfection.coeff R p 0 : (a : Perfection R p) → R) f : R) : S)
    ((Perfection.coeff S p 0 : (a : Perfection S p) → S)
        (((Perfection.map p φ : RingHom.{u₁, u₂} (Perfection R p) (Perfection S p)) :
              (a : Perfection R p) → Perfection S p)
            f :
          Perfection S p) :
      S)
⊢ Eq (α := S)
    ((Perfection.coeff S p 0 : (a : Perfection S p) → S)
        (((map p ⋯ ⋯ φ : RingHom.{u₁, u₂} (Perfection R p) (Perfection S p)) : (a : Perfection R p) → Perfection S p)
            f :
          Perfection S p) :
      S)
    ((Perfection.coeff S p 0 : (a : Perfection S p) → S)
        (((Perfection.map p φ : RingHom.{u₁, u₂} (Perfection R p) (Perfection S p)) :
              (a : Perfection R p) → Perfection S p)
            f :
          Perfection S p) :
      S)
have rw₁ : Eq.{u₂ + 1} (α := S) ((φ : (a : R) → S) ((Perfection.coeff R p 0 : (a : Perfection R p) → R) f : R) : S)
  ((φ : (a : R) → S) ((Perfection.coeff R p 0 : (a : Perfection R p) → R) f : R) : S)
Tactic: rw [map_map, Perfection.coeff_map]
-- 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
hx :
  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)}))
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) x) =
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) x)
have obtain : ∀ (r : O)
  (hr :
    r * (↑p : O) =
      Quotient.out (s := Submodule.quotientRel (R := O) (Ideal.span {(↑p : O)}))
          ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) x) -
        x),
  preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) x) =
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) x)
Tactic: obtain ⟨r, hr⟩ : ∃ (a : O), a * (p : O) = (Ideal.Quotient.mk _ x).out - x :=
    Ideal.mem_span_singleton'.1 <| Ideal.Quotient.eq.1 <| Quotient.sound' <| Quotient.mk_out' _
-- 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
hx :
  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)}))
r : O
hr :
  r * (↑p : O) =
    Quotient.out (s := Submodule.quotientRel (R := O) (Ideal.span {(↑p : O)}))
        ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) x) -
      x
⊢ preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) x) =
    (v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) x)
have refine : ¬LE.le (α := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) x) : ℝ≥0)
    ((v : (a : K) → ℝ≥0)
        (HSub.hSub (α := K) (β := K)
          ((algebraMap O K : (a : O) → K)
              (Quotient.out (s := Submodule.quotientRel (R := O) (Ideal.span {(↑p : O)}))
                ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) x)) :
            K)
          ((algebraMap O K : (a : O) → K) x : K)) :
      ℝ≥0)
Tactic: refine (if_neg hx).trans (v.map_eq_of_sub_lt <| lt_of_not_ge ?_)
-- 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
hx :
  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)}))
r : O
hr :
  r * (↑p : O) =
    Quotient.out (s := Submodule.quotientRel (R := O) (Ideal.span {(↑p : O)}))
        ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) x) -
      x
⊢ ¬LE.le (α := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) x) : ℝ≥0)
      ((v : (a : K) → ℝ≥0)
          (HSub.hSub (α := K) (β := K)
            ((algebraMap O K : (a : O) → K)
                (Quotient.out (s := Submodule.quotientRel (R := O) (Ideal.span {(↑p : O)}))
                  ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) x)) :
              K)
            ((algebraMap O K : (a : O) → K) x : K)) :
        ℝ≥0)
have rw : ¬r * (↑p : O) ∣ x
Tactic: rw [← map_sub, ← hr, hv.le_iff_dvd]
-- 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 : ℕ
y : ModP O p
hxy0 : 0 * y ≠ 0
⊢ 0 * y = 0
have rw : Eq.{u₂ + 1} (α := ModP O p) 0 0
Tactic: rw [zero_mul]
-- 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 : ℕ
x y : ModP O p
hxy0 : x * y ≠ 0
⊢ preVal K v O p (x * y) = preVal K v O p x * preVal K v O p y
have hx0 : x ≠ 0
Tactic: have hx0 : x ≠ 0 := mt (by rintro rfl; rw [zero_mul]) hxy0
-- 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 : ModP O p
hx0 : x ≠ 0
hxy0 : x * 0 ≠ 0
⊢ x * 0 = 0
have rw : Eq.{u₂ + 1} (α := ModP O p) 0 0
Tactic: rw [mul_zero]
-- 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 : ℕ
x y : ModP O p
hxy0 : x * y ≠ 0
hx0 : x ≠ 0
⊢ preVal K v O p (x * y) = preVal K v O p x * preVal K v O p y
have hy0 : y ≠ 0
Tactic: have hy0 : y ≠ 0 := mt (by rintro rfl; rw [mul_zero]) hxy0
-- 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 y : ModP O p
hxy0 : x * y ≠ 0
hx0 : x ≠ 0
hy0 : y ≠ 0
⊢ preVal K v O p (x * y) = preVal K v O p x * preVal K v O p y
have obtain : ∀ (r : O)
  (hxy0 :
    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)
  (hx0 :
    Ne (α := 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)}))
      (0 : ModP O p)),
  preVal K v O p
      (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) =
    preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r) *
      preVal K v O p y
Tactic: obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: x, hxy0, hx0
-- 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 : ℕ
y : ModP O p
hy0 : y ≠ 0
r : O
hxy0 :
  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
hx0 :
  Ne (α := 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)}))
    (0 : ModP O p)
⊢ preVal K v O p
      (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) =
    preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r) *
      preVal K v O p y
have obtain : ∀ (s : O)
  (hy0 :
    Ne (α := 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)}))
      (0 : ModP O p))
  (hxy0 :
    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),
  preVal K v 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)}))) =
    preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r) *
      preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s)
Tactic: obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective y
Cleared hypotheses: y, hy0, hxy0
-- 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 : ℕ
r : O
hx0 :
  Ne (α := 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)}))
    (0 : ModP O p)
s : O
hy0 :
  Ne (α := 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)}))
    (0 : ModP O p)
hxy0 :
  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
⊢ preVal K v 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)}))) =
    preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r) *
      preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s)
have rw : ∀
  (hxy0 :
    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)),
  preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (r * s)) =
    preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) r) *
      preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) s)
Tactic: rw [← map_mul (Ideal.Quotient.mk (Ideal.span {↑p})) r s] at hxy0 ⊢
Cleared hypotheses: hxy0