awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Perfection
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u₁
inst_1 : CommSemiring R
inst_2 : CharP R p
P : Type u₃
inst_3 : CommSemiring P
inst_4 : CharP P p
inst_5 : PerfectRing P p
π : P →+* R
m : PerfectionMap p π
⊢ @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (Perfection.coeff R p 0) (↑m.equiv : P →+* Perfection R p) = π

Tactic:
RingHom.ext fun _ => rfl

Premises used: RingHom.ext, rfl
-- Module: Mathlib.RingTheory.Perfection
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u₁
inst_1 : CommSemiring R
inst_2 : CharP R p
P : Type u₃
inst_3 : CommSemiring P
inst_4 : CharP P p
inst_5 : PerfectRing P p
π : P →+* R
m : PerfectionMap p π
f : Perfection R p
⊢ Eq.{u₁ + 1} (α := R) ((π : (a : P) → R) ((m.equiv.symm : (a : Perfection R p) → P) f : P) : R)
    ((Perfection.coeff R p 0 : (a : Perfection R p) → R) f : R)

Tactic:
(m.comp_equiv _).symm.trans <| congr_arg _ <| m.equiv.apply_symm_apply f

Premises used: RingEquiv.apply_symm_apply, PerfectionMap.equiv, congr_arg, PerfectionMap.comp_equiv, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.Perfection
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u₁
inst_1 : CommSemiring R
inst_2 : CharP R p
P : Type u₃
inst_3 : CommSemiring P
inst_4 : CharP P p
inst_5 : PerfectRing P p
π : P →+* R
m : PerfectionMap p π
⊢ Eq (α := Perfection R p →+* R) (π.comp (↑m.equiv.symm : Perfection R p →+* P)) (Perfection.coeff R p 0)

Tactic:
RingHom.ext m.comp_symm_equiv

Premises used: RingHom.ext, PerfectionMap.comp_symm_equiv
-- Module: Mathlib.RingTheory.Perfection
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
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
⊢ (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

Tactic:
simp_rw [← RingHom.comp_assoc, comp_symm_equiv']

Premises used: RingHom.comp_assoc, PerfectionMap.comp_symm_equiv'
-- Module: Mathlib.RingTheory.Perfection
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
⊢ @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (Perfection.coeff S p 0)
      ((Perfection.lift p R S : (a : R →+* S) → R →+* Perfection S p) f) =
    f

Tactic:
(Perfection.lift p R S).symm_apply_apply f

Premises used: Equiv.symm_apply_apply, Perfection.lift
-- Module: Mathlib.RingTheory.Perfection
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
⊢ @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (Perfection.coeff S p 0)
      ((Perfection.lift p R S : (a : R →+* S) → R →+* Perfection S p) f) =
    f

Tactic:
exact (Perfection.lift p R S).symm_apply_apply f

Premises used: Equiv.symm_apply_apply, Perfection.lift
-- Module: Mathlib.RingTheory.Perfection
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
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)
⊢ 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))

Tactic:
rw [Equiv.apply_eq_iff_eq_symm_apply]

Premises used: Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.RingTheory.Perfection
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
⊢ π.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:
rfl
-- Module: Mathlib.RingTheory.Perfection
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
⊢ (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))
      ((fun (f : R →+* P) ↦ π.comp f) f) =
    f

Tactic:
exact RingHom.ext fun x => m.equiv.injective <| (m.equiv.apply_symm_apply _).trans
      <| show Perfection.lift p R S (π.comp f) x = RingHom.comp (↑m.equiv) f x from
        RingHom.ext_iff.1 (by rw [Equiv.apply_eq_iff_eq_symm_apply]; rfl) _

Premises used: RingEquiv.injective, PerfectionMap.equiv, RingHom.ext
-- Module: Mathlib.RingTheory.Perfection
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u₁
inst_1 : CommSemiring R
inst_2 : CharP R p
inst_3 : PerfectRing R p
S : Type u₂
inst_4 : CommSemiring S
inst_5 : CharP S p
P : Type u₃
inst_6 : CommSemiring P
inst_7 : CharP P p
inst_8 : PerfectRing P p
π : P →+* S
m : PerfectionMap p π
f g : R →+* P
hfg :
  ∀ (x : R),
    Eq.{u₂ + 1} (α := S) ((π : (a : P) → S) ((f : (a : R) → P) x : P) : S)
      ((π : (a : P) → S) ((g : (a : R) → P) x : P) : S)
⊢ f = g

Tactic:
(lift p R S P π m).symm.injective <| RingHom.ext hfg

Premises used: RingHom.ext, PerfectionMap.lift, Equiv.injective, Equiv.symm
-- Module: Mathlib.RingTheory.Perfection
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u₁
inst_1 : CommSemiring R
inst_2 : CharP R p
P : Type u₃
inst_3 : CommSemiring P
inst_4 : CharP P p
inst_5 : PerfectRing P p
S : Type u₂
inst_6 : CommSemiring S
inst_7 : CharP S p
Q : Type u₄
inst_8 : CommSemiring Q
inst_9 : CharP Q p
inst_10 : PerfectRing Q p
π : P →+* R
m : PerfectionMap p π
σ : Q →+* S
n : PerfectionMap p σ
φ : R →+* S
⊢ σ.comp (map p m n φ) = φ.comp π

Tactic:
(lift p P S Q σ n).symm_apply_apply _

Premises used: Equiv.symm_apply_apply, PerfectionMap.lift
-- Module: Mathlib.RingTheory.Perfection
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u₁
inst_1 : CommSemiring R
inst_2 : CharP R p
P : Type u₃
inst_3 : CommSemiring P
inst_4 : CharP P p
inst_5 : PerfectRing P p
S : Type u₂
inst_6 : CommSemiring S
inst_7 : CharP S p
Q : Type u₄
inst_8 : CommSemiring Q
inst_9 : CharP Q p
inst_10 : PerfectRing Q p
π : P →+* R
m : PerfectionMap p π
σ : Q →+* S
n : PerfectionMap p σ
φ : R →+* S
x : P
⊢ Eq.{u₂ + 1} (α := S) ((σ : (a : Q) → S) ((map p m n φ : (a : P) → Q) x : Q) : S)
    ((φ : (a : R) → S) ((π : (a : P) → R) x : R) : S)

Tactic:
RingHom.ext_iff.1 (comp_map p m n φ) x

Premises used: RingHom.ext_iff, Iff.mp, PerfectionMap.comp_map
-- Module: Mathlib.RingTheory.Perfection
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [map_map, Perfection.coeff_map]

Premises used: Perfection.coeff_map, PerfectionMap.map_map
-- Module: Mathlib.RingTheory.Perfection
Goal:
O : Type u₂
inst : CommRing O
p : ℕ
inst_1 : Fact (Nat.Prime p)
hvp : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
⊢ CharP.{u₂} (ModP O p) p

Tactic:
CharP.quotient O p <| hvp.1

Premises used: CharP.quotient, Fact.out
-- Module: Mathlib.RingTheory.Perfection
Goal:
O : Type u₂
inst : CommRing O
p : ℕ
hp : Fact (Nat.Prime p)
inst_1 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
⊢ Nontrivial.{u₂} (ModP O p)

Tactic:
CharP.nontrivial_of_char_ne_one hp.1.ne_one

Premises used: CharP.nontrivial_of_char_ne_one, Nat.Prime.ne_one, Fact.out
-- 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
p : ℕ
⊢ preVal K v O p 0 = 0

Tactic:
if_pos rfl

Premises used: ModP.preVal, if_pos, 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 : ℕ
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)}))
⊢ ∃ (a : O),
    a * (↑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

Tactic:
Ideal.mem_span_singleton'.1 <| Ideal.Quotient.eq.1 <| Quotient.sound' <| Quotient.mk_out' _

Premises used: Quotient.sound', Ideal.mem_span_singleton', Ideal.Quotient.eq, Iff.mp, Quotient.mk_out'
-- 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
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)}))
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)
⊢ 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' _

Premises used: Quotient.sound', Ideal.mem_span_singleton', Ideal.Quotient.mk, Quotient.out, Nat.cast, Ideal.Quotient.eq, Iff.mp, Quotient.mk_out', 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 : ℕ
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)

Tactic:
(if_neg hx).trans (v.map_eq_of_sub_lt <| lt_of_not_ge ?_)

Premises used: lt_of_not_ge, ModP.preVal, Valuation.map_eq_of_sub_lt, if_neg, Eq.trans
-- 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
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
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)
⊢ 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:
refine (if_neg hx).trans (v.map_eq_of_sub_lt <| lt_of_not_ge ?_)

Premises used: lt_of_not_ge, Valuation.map_eq_of_sub_lt, if_neg, Eq.trans
-- 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
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
rw : ¬r * (↑p : O) ∣ 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)

Tactic:
rw [← map_sub, ← hr, hv.le_iff_dvd]

Premises used: map_sub, Valuation.Integers.le_iff_dvd
-- 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
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
⊢ ¬r * (↑p : O) ∣ x

Tactic:
fun hprx =>
    hx (Ideal.Quotient.eq_zero_iff_mem.2 <| Ideal.mem_span_singleton.2 <| dvd_of_mul_left_dvd hprx)

Premises used: Iff.mpr, dvd_of_mul_left_dvd, Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton, Not
-- 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
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
⊢ ¬r * (↑p : O) ∣ x

Tactic:
exact fun hprx =>
    hx (Ideal.Quotient.eq_zero_iff_mem.2 <| Ideal.mem_span_singleton.2 <| dvd_of_mul_left_dvd hprx)

Premises used: Iff.mpr, dvd_of_mul_left_dvd, Ideal.Quotient.eq_zero_iff_mem, 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 : ℕ
y : ModP O p
hxy0 : 0 * y ≠ 0
rw rw₁ : Eq.{u₂ + 1} (α := ModP O p) 0 0
⊢ 0 * y = 0

Tactic:
rw [zero_mul]

Premises used: MulZeroClass.zero_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 : ℕ
x y : ModP O p
hxy0 : x * y ≠ 0
⊢ x ≠ 0

Tactic:
have hx0 : x ≠ 0 := mt (by rintro rfl; rw [zero_mul]) hxy0
-- 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 : ModP O p
hx0 : x ≠ 0
hxy0 : x * 0 ≠ 0
rw rw₁ : Eq.{u₂ + 1} (α := ModP O p) 0 0
⊢ x * 0 = 0

Tactic:
rw [mul_zero]

Premises used: MulZeroClass.mul_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 : ℕ
x y : ModP O p
hxy0 : x * y ≠ 0
hx0 : x ≠ 0
⊢ y ≠ 0

Tactic:
have hy0 : y ≠ 0 := mt (by rintro rfl; rw [mul_zero]) hxy0
-- 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 y : ModP O p
hxy0 : x * y ≠ 0
hx0 : x ≠ 0
hy0 : y ≠ 0
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
⊢ preVal K v O p (x * y) = preVal K v O p x * preVal K v O p y

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 : ℕ
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)
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)
⊢ 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 ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective y

Premises used: Ideal.Quotient.mk_surjective, rfl