awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun (n : ℕ) ↦ peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun (n : ℕ) ↦ peval (ψ n) ![x.coeff, y.coeff]
R : Type u
_Rcr : CommRing R
x_1 y : 𝕎 R
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  Eq.{u + 1} (α := ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
            (coeff
              (f (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ })
                (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ }))) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
    ((eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
            (coeff
              (g (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ })
                (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ }))) :
          (a : MvPolynomial ℕ ℤ) → ULift.{u, 0} ℤ)
        (wittPolynomial p ℤ k) :
      ULift.{u, 0} ℤ)
x_2 : ℕ
apply :
  Eq.{max 1 (u + 1)} (α := Fin 2 × ℕ → ULift.{u, 0} ℤ)
    (fun (i : Fin 2 × ℕ) ↦
      ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x i))
    (uncurry
      ![coeff (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ }),
        coeff (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ })])
⊢ Eq (α := ULift.{u, 0} ℤ)
    ((eval₂Hom (RingHom.comp (↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) (RingHom.id ℤ))
            fun (i : Fin 2 × ℕ) ↦
            ((↑(RingEquiv.symm ULift.ringEquiv) : ℤ →+* ULift.{u, 0} ℤ) : (a : ℤ) → ULift.{u, 0} ℤ) (x i) :
          (a : MvPolynomial (Fin 2 × ℕ) ℤ) → ULift.{u, 0} ℤ)
        (ψ x_2) :
      ULift.{u, 0} ℤ)
    (peval (ψ x_2)
        ![coeff (mk p fun (i : ℕ) ↦ { down := x (0, i) : ULift.{u, 0} ℤ }),
          coeff (mk p fun (i : ℕ) ↦ { down := x (1, i) : ULift.{u, 0} ℤ })] :
      ULift.{u, 0} ℤ)

Tactic:
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl

Premises used: MvPolynomial.eval₂Hom_congr, RingHom.ext_int, rfl
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
hf : IsPoly₂ p f
g : R →+* S
x y : 𝕎 R
obtain :
  ∀ (φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ)
    (hf :
      ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun (n : ℕ) ↦ peval (φ n) ![x.coeff, y.coeff]),
    Eq (α := 𝕎 S) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) (f x y) : 𝕎 S)
      (f ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) y) : 𝕎 S)
⊢ Eq (α := 𝕎 S) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) (f x y) : 𝕎 S)
    (f ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) y) : 𝕎 S)

Tactic:
obtain ⟨φ, hf⟩ := hf
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun (n : ℕ) ↦ peval (φ n) ![x.coeff, y.coeff]
h :
  ∀ (n : ℕ),
    Eq.{u + 1} (α := S) (coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) (f x y)) n)
      (coeff (f ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) y)) n)
⊢ Eq (α := 𝕎 S) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) (f x y) : 𝕎 S)
    (f ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) y) : 𝕎 S)

Tactic:
ext n
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun (n : ℕ) ↦ peval (φ n) ![x.coeff, y.coeff]
n : ℕ
h :
  Eq (α := S)
    ((eval₂Hom (g.comp (algebraMap ℤ R)) fun (i : Fin 2 × ℕ) ↦ (g : (a : R) → S) (![x.coeff, y.coeff] i.1 i.2) :
          (a : MvPolynomial (Fin 2 × ℕ) ℤ) → S)
        (φ n) :
      S)
    (((aeval.{0, u, 0} (R := ℤ) (S₁ := S) fun (a : Fin 2 × ℕ) ↦
              ![coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x),
                  coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) y)]
                a.1 a.2 :
            MvPolynomial (Fin 2 × ℕ) ℤ →ₐ[ℤ] S) :
          (a : MvPolynomial (Fin 2 × ℕ) ℤ) → S)
        (φ n) :
      S)
⊢ Eq.{u + 1} (α := S) (coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) (f x y)) n)
    (coeff (f ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) y)) n)

Tactic:
simp +unfoldPartialApp only [map_coeff, hf, map_aeval, peval, uncurry]

Premises used: WittVector.map_coeff, WittVector.peval, MvPolynomial.map_aeval, Function.uncurry
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun (n : ℕ) ↦ peval (φ n) ![x.coeff, y.coeff]
n : ℕ
apply :
  Eq.{max 1 (u + 1)} (α := Fin 2 × ℕ → S) (fun (i : Fin 2 × ℕ) ↦ (g : (a : R) → S) (![x.coeff, y.coeff] i.1 i.2))
    fun (a : Fin 2 × ℕ) ↦
    ![coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x), coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) y)]
      a.1 a.2
⊢ Eq (α := S)
    ((eval₂Hom (g.comp (algebraMap ℤ R)) fun (i : Fin 2 × ℕ) ↦ (g : (a : R) → S) (![x.coeff, y.coeff] i.1 i.2) :
          (a : MvPolynomial (Fin 2 × ℕ) ℤ) → S)
        (φ n) :
      S)
    (((aeval.{0, u, 0} (R := ℤ) (S₁ := S) fun (a : Fin 2 × ℕ) ↦
              ![coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x),
                  coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) y)]
                a.1 a.2 :
            MvPolynomial (Fin 2 × ℕ) ℤ →ₐ[ℤ] S) :
          (a : MvPolynomial (Fin 2 × ℕ) ℤ) → S)
        (φ n) :
      S)

Tactic:
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl

Premises used: MvPolynomial.eval₂Hom_congr, RingHom.ext_int, rfl
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun (n : ℕ) ↦ peval (φ n) ![x.coeff, y.coeff]
n : ℕ
h :
  ∀ (i : Fin 2) (k : ℕ),
    Eq (α := S) ((g : (a : R) → S) (![x.coeff, y.coeff] (i, k).1 (i, k).2) : S)
      (![coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x),
            coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) y)]
          (i, k).1 (i, k).2 :
        S)
⊢ Eq.{max 1 (u + 1)} (α := Fin 2 × ℕ → S) (fun (i : Fin 2 × ℕ) ↦ (g : (a : R) → S) (![x.coeff, y.coeff] i.1 i.2))
    fun (a : Fin 2 × ℕ) ↦
    ![coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x), coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) y)]
      a.1 a.2

Tactic:
ext ⟨i, k⟩
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun (n : ℕ) ↦ peval (φ n) ![x.coeff, y.coeff]
n : ℕ
i : Fin 2
k : ℕ
h :
  Eq (α := S)
    ((g : (a : R) → S)
        (![x.coeff, y.coeff] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), k).1
          ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), k).2) :
      S)
    (![coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x), coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) y)]
        ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), k).1 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩, k).2 :
      S)
h₁ :
  Eq (α := S)
    ((g : (a : R) → S)
        (![x.coeff, y.coeff] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2), k).1
          ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2), k).2) :
      S)
    (![coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x), coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) y)]
        ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2), k).1 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩, k).2 :
      S)
⊢ Eq (α := S) ((g : (a : R) → S) (![x.coeff, y.coeff] (i, k).1 (i, k).2) : S)
    (![coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x), coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) y)]
        (i, k).1 (i, k).2 :
      S)

Tactic:
fin_cases i
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun (n : ℕ) ↦ peval (φ n) ![x.coeff, y.coeff]
n k : ℕ
⊢ Eq (α := S)
    ((g : (a : R) → S)
        (![x.coeff, y.coeff] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), k).1
          ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), k).2) :
      S)
    (![coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x), coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) y)]
        ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2), k).1 ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩, k).2 :
      S)

Tactic:
simp
-- Module: Mathlib.RingTheory.WittVector.IsPoly
Goal:
p : ℕ
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
g : R →+* S
x y : 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun (n : ℕ) ↦ peval (φ n) ![x.coeff, y.coeff]
n k : ℕ
⊢ Eq (α := S)
    ((g : (a : R) → S)
        (![x.coeff, y.coeff] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2), k).1
          ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2), k).2) :
      S)
    (![coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) x), coeff (p := p) ((WittVector.map g : (a : 𝕎 R) → 𝕎 S) y)]
        ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2), k).1 ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩, k).2 :
      S)

Tactic:
simp
-- Module: Mathlib.RingTheory.WittVector.Isocrystal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_1
inst_1 : CommRing k
inst_2 : IsDomain k
inst_3 : CharP k p
inst_4 : PerfectRing k p
⊢ RingHomInvPair φ(p, k) (↑(RingEquiv.symm (FractionRing.frobenius p k)) : K(p, k) →+* K(p, k))

Tactic:
RingHomInvPair.of_ringEquiv (FractionRing.frobenius p k)

Premises used: WittVector.FractionRing.frobenius, RingHomInvPair.of_ringEquiv, WittVector.FractionRing.frobeniusRingHom
-- Module: Mathlib.RingTheory.WittVector.Isocrystal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_1
inst_1 : CommRing k
inst_2 : IsDomain k
inst_3 : CharP k p
inst_4 : PerfectRing k p
⊢ RingHomInvPair (↑(RingEquiv.symm (FractionRing.frobenius p k)) : K(p, k) →+* K(p, k))
    (↑(FractionRing.frobenius p k) : K(p, k) →+* K(p, k))

Tactic:
RingHomInvPair.of_ringEquiv (FractionRing.frobenius p k).symm

Premises used: WittVector.FractionRing.frobenius, IsFractionRing.ringEquivOfRingEquiv, IsLocalization.ringEquivOfRingEquiv, RingHomInvPair.of_ringEquiv, Equiv.symm, RingEquiv.symm
-- Module: Mathlib.RingTheory.WittVector.Isocrystal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_1
inst_1 : CommRing k
inst_2 : IsDomain k
inst_3 : CharP k p
inst_4 : PerfectRing k p
m : ℤ
x : StandardOneDimIsocrystal p k m
⊢ (Φ(p, k) : (a : StandardOneDimIsocrystal p k m) → StandardOneDimIsocrystal p k m) x =
    HSMul.hSMul (β := K(p, k)) (HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m)
      ((φ(p, k) : (a : K(p, k)) → K(p, k)) x : K(p, k))

Tactic:
rfl

Premises used: Set.Mem, OreLocalization.liftExpand, rfl
-- Module: Mathlib.RingTheory.WittVector.Isocrystal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_2
inst_1 : Field k
inst_2 : IsAlgClosed k
inst_3 : CharP k p
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Isocrystal p k V
h_dim : finrank.{u_2, u_3} K(p, k) V = 1
⊢ Nontrivial V

Tactic:
haveI : Nontrivial V := Module.nontrivial_of_finrank_eq_succ h_dim
-- Module: Mathlib.RingTheory.WittVector.Isocrystal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_2
inst_1 : Field k
inst_2 : IsAlgClosed k
inst_3 : CharP k p
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Isocrystal p k V
h_dim : finrank.{u_2, u_3} K(p, k) V = 1
this : Nontrivial V
⊢ ∃ (x : V), x ≠ 0

Tactic:
exists_ne 0

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.RingTheory.WittVector.Isocrystal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_2
inst_1 : Field k
inst_2 : IsAlgClosed k
inst_3 : CharP k p
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Isocrystal p k V
h_dim : finrank.{u_2, u_3} K(p, k) V = 1
this : Nontrivial V
obtain : ∀ (x : V) (hx : x ≠ 0), ∃ (m : ℤ), Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
⊢ ∃ (m : ℤ), Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)

Tactic:
obtain ⟨x, hx⟩ : ∃ x : V, x ≠ 0 := exists_ne 0

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.RingTheory.WittVector.Isocrystal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_2
inst_1 : Field k
inst_2 : IsAlgClosed k
inst_3 : CharP k p
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Isocrystal p k V
h_dim : finrank.{u_2, u_3} K(p, k) V = 1
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ Ne (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)

Tactic:
simpa only [map_zero] using Φ(p, k).injective.ne hx

Premises used: WittVector.Isocrystal.frobenius, Function.Injective.ne, map_zero, LinearEquiv.injective
-- Module: Mathlib.RingTheory.WittVector.Isocrystal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_2
inst_1 : Field k
inst_2 : IsAlgClosed k
inst_3 : CharP k p
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Isocrystal p k V
h_dim : finrank.{u_2, u_3} K(p, k) V = 1
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ Ne (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)

Tactic:
have : Φ(p, k) x ≠ 0 := by simpa only [map_zero] using Φ(p, k).injective.ne hx
-- Module: Mathlib.RingTheory.WittVector.Isocrystal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_2
inst_1 : Field k
inst_2 : IsAlgClosed k
inst_3 : CharP k p
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Isocrystal p k V
h_dim : finrank.{u_2, u_3} K(p, k) V = 1
this_1 : Nontrivial V
x : V
hx : x ≠ 0
this : Ne (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)
⊢ ∀ (w : V), ∃ (c : K(p, k)), c • x = w

Tactic:
rw [finrank_eq_one_iff_of_nonzero' x hx] at h_dim

Premises used: finrank_eq_one_iff_of_nonzero'
-- Module: Mathlib.RingTheory.WittVector.Isocrystal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_2
inst_1 : Field k
inst_2 : IsAlgClosed k
inst_3 : CharP k p
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Isocrystal p k V
h_dim : finrank.{u_2, u_3} K(p, k) V = 1
this_1 : Nontrivial V
x : V
hx : x ≠ 0
this : Ne (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)
h_dim₁ : ∀ (w : V), ∃ (c : K(p, k)), c • x = w
⊢ x ≠ 0

Tactic:
rw [finrank_eq_one_iff_of_nonzero' x hx] at h_dim

Premises used: finrank_eq_one_iff_of_nonzero'
-- Module: Mathlib.RingTheory.WittVector.Isocrystal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_2
inst_1 : Field k
inst_2 : IsAlgClosed k
inst_3 : CharP k p
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Isocrystal p k V
h_dim : finrank.{u_2, u_3} K(p, k) V = 1
this_1 : Nontrivial V
x : V
hx : x ≠ 0
this : Ne (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)
h_dim₁ : ∀ (w : V), ∃ (c : K(p, k)), c • x = w
hx₁ : x ≠ 0
⊢ Ne (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)

Tactic:
rw [finrank_eq_one_iff_of_nonzero' x hx] at h_dim

Premises used: finrank_eq_one_iff_of_nonzero'
-- Module: Mathlib.RingTheory.WittVector.Isocrystal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_2
inst_1 : Field k
inst_2 : IsAlgClosed k
inst_3 : CharP k p
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Isocrystal p k V
this_1 : Nontrivial V
x : V
h_dim : ∀ (w : V), ∃ (c : K(p, k)), c • x = w
hx : x ≠ 0
this : Ne (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)
obtain :
  ∀ (a : K(p, k)) (ha : a • x = (Φ(p, k) : (a : V) → V) x), ∃ (a : K(p, k)), a ≠ 0 ∧ (Φ(p, k) : (a : V) → V) x = a • x
⊢ ∃ (a : K(p, k)), a ≠ 0 ∧ (Φ(p, k) : (a : V) → V) x = a • x

Tactic:
obtain ⟨a, ha⟩ := h_dim (Φ(p, k) x)

Premises used: WittVector.Isocrystal.frobenius, DFunLike.coe
-- Module: Mathlib.RingTheory.WittVector.Isocrystal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_2
inst_1 : Field k
inst_2 : IsAlgClosed k
inst_3 : CharP k p
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Isocrystal p k V
this_1 : Nontrivial V
x : V
h_dim : ∀ (w : V), ∃ (c : K(p, k)), c • x = w
hx : x ≠ 0
this : Ne (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)
a : K(p, k)
ha : a • x = (Φ(p, k) : (a : V) → V) x
⊢ ∃ (a : K(p, k)), a ≠ 0 ∧ (Φ(p, k) : (a : V) → V) x = a • x

Tactic:
⟨a, ?_, ha.symm⟩

Premises used: And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.RingTheory.WittVector.Isocrystal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_2
inst_1 : Field k
inst_2 : IsAlgClosed k
inst_3 : CharP k p
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Isocrystal p k V
this_1 : Nontrivial V
x : V
h_dim : ∀ (w : V), ∃ (c : K(p, k)), c • x = w
hx : x ≠ 0
this : Ne (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)
a : K(p, k)
ha : a • x = (Φ(p, k) : (a : V) → V) x
refine : a ≠ 0
⊢ ∃ (a : K(p, k)), a ≠ 0 ∧ (Φ(p, k) : (a : V) → V) x = a • x

Tactic:
refine ⟨a, ?_, ha.symm⟩
-- Module: Mathlib.RingTheory.WittVector.Isocrystal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_2
inst_1 : Field k
inst_2 : IsAlgClosed k
inst_3 : CharP k p
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Isocrystal p k V
this_1 : Nontrivial V
x : V
h_dim : ∀ (w : V), ∃ (c : K(p, k)), c • x = w
hx : x ≠ 0
this : Ne (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)
a : K(p, k)
ha : a • x = (Φ(p, k) : (a : V) → V) x
ha' : a = 0
apply : Eq (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)
⊢ False

Tactic:
apply this
-- Module: Mathlib.RingTheory.WittVector.Isocrystal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_2
inst_1 : Field k
inst_2 : IsAlgClosed k
inst_3 : CharP k p
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Isocrystal p k V
this_1 : Nontrivial V
x : V
h_dim : ∀ (w : V), ∃ (c : K(p, k)), c • x = w
hx : x ≠ 0
this : Ne (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)
a : K(p, k)
ha : a • x = (Φ(p, k) : (a : V) → V) x
ha' : a = 0
⊢ Eq (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)

Tactic:
simp only [← ha, ha', zero_smul]

Premises used: zero_smul
-- Module: Mathlib.RingTheory.WittVector.Isocrystal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_2
inst_1 : Field k
inst_2 : IsAlgClosed k
inst_3 : CharP k p
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Isocrystal p k V
h_dim : finrank.{u_2, u_3} K(p, k) V = 1
this_1 : Nontrivial V
x : V
hx : x ≠ 0
this : Ne (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)
obtain :
  ∀ (a : K(p, k)) (ha : a ≠ 0) (hax : (Φ(p, k) : (a : V) → V) x = a • x),
    ∃ (m : ℤ), Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
⊢ ∃ (m : ℤ), Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)

Tactic:
obtain ⟨a, ha, hax⟩ : ∃ a : K(p, k), a ≠ 0 ∧ Φ(p, k) x = a • x := by
    rw [finrank_eq_one_iff_of_nonzero' x hx] at h_dim
    obtain ⟨a, ha⟩ := h_dim (Φ(p, k) x)
    refine ⟨a, ?_, ha.symm⟩
    intro ha'
    apply this
    simp only [← ha, ha', zero_smul]

Premises used: WittVector.Isocrystal.frobenius, DFunLike.coe
-- Module: Mathlib.RingTheory.WittVector.Isocrystal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_2
inst_1 : Field k
inst_2 : IsAlgClosed k
inst_3 : CharP k p
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Isocrystal p k V
h_dim : finrank.{u_2, u_3} K(p, k) V = 1
this_1 : Nontrivial V
x : V
hx : x ≠ 0
this : Ne (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)
a : K(p, k)
ha : a ≠ 0
hax : (Φ(p, k) : (a : V) → V) x = a • x
obtain :
  ∀ (b : K(p, k)) (hb : b ≠ 0) (m : ℤ)
    (hmb :
      HMul.hMul (α := K(p, k))
          ((IsFractionRing.ringEquivOfRingEquiv (A := WittVector p k) (B := WittVector p k) (frobeniusEquiv p k) :
                (a : K(p, k)) → K(p, k))
              b :
            K(p, k))
          a =
        HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m * b),
    ∃ (m : ℤ), Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
⊢ ∃ (m : ℤ), Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)

Tactic:
obtain ⟨b, hb, m, hmb⟩ := WittVector.exists_frobenius_solution_fractionRing p ha

Premises used: WittVector.exists_frobenius_solution_fractionRing
-- Module: Mathlib.RingTheory.WittVector.Isocrystal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_2
inst_1 : Field k
inst_2 : IsAlgClosed k
inst_3 : CharP k p
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Isocrystal p k V
h_dim : finrank.{u_2, u_3} K(p, k) V = 1
this_1 : Nontrivial V
x : V
hx : x ≠ 0
this : Ne (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)
a : K(p, k)
ha : a ≠ 0
hax : (Φ(p, k) : (a : V) → V) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb :
  HMul.hMul (α := K(p, k))
      ((IsFractionRing.ringEquivOfRingEquiv (A := WittVector p k) (B := WittVector p k) (frobeniusEquiv p k) :
            (a : K(p, k)) → K(p, k))
          b :
        K(p, k))
      a =
    HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m * b
⊢ HMul.hMul (α := K(p, k))
      ((IsFractionRing.ringEquivOfRingEquiv (A := WittVector p k) (B := WittVector p k) (frobeniusEquiv p k) :
            (a : K(p, k)) → K(p, k))
          b :
        K(p, k))
      a =
    HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m * b

Tactic:
hmb
-- Module: Mathlib.RingTheory.WittVector.Isocrystal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_2
inst_1 : Field k
inst_2 : IsAlgClosed k
inst_3 : CharP k p
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Isocrystal p k V
h_dim : finrank.{u_2, u_3} K(p, k) V = 1
this_1 : Nontrivial V
x : V
hx : x ≠ 0
this : Ne (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)
a : K(p, k)
ha : a ≠ 0
hax : (Φ(p, k) : (a : V) → V) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb :
  HMul.hMul (α := K(p, k))
      ((IsFractionRing.ringEquivOfRingEquiv (A := WittVector p k) (B := WittVector p k) (frobeniusEquiv p k) :
            (a : K(p, k)) → K(p, k))
          b :
        K(p, k))
      a =
    HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m * b
⊢ HMul.hMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) b : K(p, k)) a =
    HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m * b

Tactic:
convert! hmb
-- Module: Mathlib.RingTheory.WittVector.Isocrystal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_2
inst_1 : Field k
inst_2 : IsAlgClosed k
inst_3 : CharP k p
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Isocrystal p k V
h_dim : finrank.{u_2, u_3} K(p, k) V = 1
this_1 : Nontrivial V
x : V
hx : x ≠ 0
this : Ne (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)
a : K(p, k)
ha : a ≠ 0
hax : (Φ(p, k) : (a : V) → V) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb :
  HMul.hMul (α := K(p, k))
      ((IsFractionRing.ringEquivOfRingEquiv (A := WittVector p k) (B := WittVector p k) (frobeniusEquiv p k) :
            (a : K(p, k)) → K(p, k))
          b :
        K(p, k))
      a =
    HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m * b
⊢ HMul.hMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) b : K(p, k)) a =
    HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m * b

Tactic:
replace hmb : φ(p, k) b * a = (p : K(p, k)) ^ m * b := by convert! hmb
-- Module: Mathlib.RingTheory.WittVector.Isocrystal
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_2
inst_1 : Field k
inst_2 : IsAlgClosed k
inst_3 : CharP k p
V : Type u_3
inst_4 : AddCommGroup V
inst_5 : Isocrystal p k V
h_dim : finrank.{u_2, u_3} K(p, k) V = 1
this_1 : Nontrivial V
x : V
hx : x ≠ 0
this : Ne (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)
a : K(p, k)
ha : a ≠ 0
hax : (Φ(p, k) : (a : V) → V) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb :
  HMul.hMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) b : K(p, k)) a =
    HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m * b
h : Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
⊢ ∃ (m : ℤ), Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)

Tactic:
use m