awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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]
⊢ 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)
have 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)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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 : ℕ
⊢ 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)
have 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)
Tactic: simp +unfoldPartialApp only [map_coeff, hf, map_aeval, peval, uncurry]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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 : ℕ
⊢ 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)
have 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
Tactic: apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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 : ℕ
⊢ 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
have 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)
Tactic: ext ⟨i, k⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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 : ℕ
⊢ 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)
have h : Eq (α := S)
  ((g : (a : R) → S)
      (![x.coeff, y.coeff] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2), k).1
        ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : 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, sorry⟩ : Fin 2), k).1 ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩, k).2 :
    S)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.IsPoly (goal)
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)
⊢ 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)
have h₁ : Eq (α := S)
  ((g : (a : R) → S)
      (![x.coeff, y.coeff] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2), k).1
        ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : 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, sorry⟩ : Fin 2), k).1 ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩, k).2 :
    S)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Isocrystal (hypothesis)
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
⊢ ∃ (m : ℤ), Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
have this : Nontrivial V
Tactic: haveI : Nontrivial V := Module.nontrivial_of_finrank_eq_succ h_dim
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Isocrystal (goal)
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
⊢ ∃ (m : ℤ), Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
have obtain : ∀ (x : V) (hx : x ≠ 0), ∃ (m : ℤ), Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
Tactic: obtain ⟨x, hx⟩ : ∃ x : V, x ≠ 0 := exists_ne 0
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Isocrystal (hypothesis)
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
⊢ ∃ (m : ℤ), Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Isocrystal (hypothesis)
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)), a ≠ 0 ∧ (Φ(p, k) : (a : V) → V) x = a • x
have h_dim₁ : ∀ (w : V), ∃ (c : K(p, k)), c • x = w
Tactic: rw [finrank_eq_one_iff_of_nonzero' x hx] at h_dim
Cleared hypotheses: h_dim, hx, this
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Isocrystal (goal)
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)), a ≠ 0 ∧ (Φ(p, k) : (a : V) → V) x = a • x
have 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
Tactic: obtain ⟨a, ha⟩ := h_dim (Φ(p, k) x)
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Isocrystal (goal)
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
have refine : a ≠ 0
Tactic: refine ⟨a, ?_, ha.symm⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Isocrystal (goal)
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
⊢ False
have apply : Eq (α := V) ((Φ(p, k) : (a : V) → V) x : V) (0 : V)
Tactic: apply this
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Isocrystal (goal)
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)
⊢ ∃ (m : ℤ), Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Isocrystal (goal)
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
⊢ ∃ (m : ℤ), Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
have 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)
Tactic: obtain ⟨b, hb, m, hmb⟩ := WittVector.exists_frobenius_solution_fractionRing p ha
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Isocrystal (hypothesis)
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
⊢ ∃ (m : ℤ), Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
have 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
Tactic: replace hmb : φ(p, k) b * a = (p : K(p, k)) ^ m * b := by convert! hmb
Cleared hypotheses: hmb
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Isocrystal (goal)
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
⊢ ∃ (m : ℤ), Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
have h : Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
Tactic: use m
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Isocrystal (goal)
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
F₀ : LinearMap.{u_2, u_2, u_2, u_3} (R := K(p, k)) (RingHom.id K(p, k)) (StandardOneDimIsocrystal p k m) V :=
  LinearMap.toSpanSingleton K(p, k) V x
⊢ StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V
have refine_1 : Function.Injective.{u_2 + 1, u_3 + 1} (α := StandardOneDimIsocrystal p k m) (β := V)
  (⇑F₀ : (a : StandardOneDimIsocrystal p k m) → V)
Tactic: refine LinearEquiv.ofBijective F₀ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Isocrystal (goal)
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
F₀ : LinearMap.{u_2, u_2, u_2, u_3} (R := K(p, k)) (RingHom.id K(p, k)) (StandardOneDimIsocrystal p k m) V :=
  LinearMap.toSpanSingleton K(p, k) V x
refine_1 :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := StandardOneDimIsocrystal p k m) (β := V)
    (⇑F₀ : (a : StandardOneDimIsocrystal p k m) → V)
⊢ StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V
have refine_2 : Function.Surjective.{u_2 + 1, u_3 + 1} (α := StandardOneDimIsocrystal p k m) (β := V)
  (⇑F₀ : (a : StandardOneDimIsocrystal p k m) → V)
Tactic: refine LinearEquiv.ofBijective F₀ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Isocrystal (goal)
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
F₀ : LinearMap.{u_2, u_2, u_2, u_3} (R := K(p, k)) (RingHom.id K(p, k)) (StandardOneDimIsocrystal p k m) V :=
  LinearMap.toSpanSingleton K(p, k) V x
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := StandardOneDimIsocrystal p k m) (β := V)
    (⇑F₀ : (a : StandardOneDimIsocrystal p k m) → V)
have refine_1 : F₀.ker = ⊥
Tactic: rw [← LinearMap.ker_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Isocrystal (goal)
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
F₀ : LinearMap.{u_2, u_2, u_2, u_3} (R := K(p, k)) (RingHom.id K(p, k)) (StandardOneDimIsocrystal p k m) V :=
  LinearMap.toSpanSingleton K(p, k) V x
⊢ Function.Surjective.{u_2 + 1, u_3 + 1} (α := StandardOneDimIsocrystal p k m) (β := V)
    (⇑F₀ : (a : StandardOneDimIsocrystal p k m) → V)
have refine_2 : F₀.range = ⊤
Tactic: rw [← LinearMap.range_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Isocrystal (goal)
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
F₀ : LinearMap.{u_2, u_2, u_2, u_3} (R := K(p, k)) (RingHom.id K(p, k)) (StandardOneDimIsocrystal p k m) V :=
  LinearMap.toSpanSingleton K(p, k) V x
⊢ F₀.range = ⊤
have refine_2 : F₀.range = K(p, k) ∙ x
Tactic: rw [← (finrank_eq_one_iff_of_nonzero x hx).mp h_dim]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Isocrystal (goal)
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
F₀ : LinearMap.{u_2, u_2, u_2, u_3} (R := K(p, k)) (RingHom.id K(p, k)) (StandardOneDimIsocrystal p k m) V :=
  LinearMap.toSpanSingleton K(p, k) V x
⊢ F₀.range = K(p, k) ∙ x
have refine_2 : F₀.range = LinearMap.range (LinearMap.toSpanSingleton K(p, k) V x)
Tactic: rw [LinearMap.span_singleton_eq_range]
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Isocrystal (goal)
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
F₀ : LinearMap.{u_2, u_2, u_2, u_3} (R := K(p, k)) (RingHom.id K(p, k)) (StandardOneDimIsocrystal p k m) V :=
  LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯
⊢ Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
have h : ∀ (c : StandardOneDimIsocrystal p k m),
  Eq (α := V)
    ((Φ(p, k) : (a : V) → V)
        ((LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb ≪≫ₗ F :
              (a : StandardOneDimIsocrystal p k m) → V)
            c :
          V) :
      V)
    ((LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb ≪≫ₗ F :
          (a : StandardOneDimIsocrystal p k m) → V)
        ((Φ(p, k) : (a : StandardOneDimIsocrystal p k m) → StandardOneDimIsocrystal p k m) c :
          StandardOneDimIsocrystal p k m) :
      V)
Tactic: refine ⟨⟨(LinearEquiv.smulOfNeZero K(p, k) _ _ hb).trans F, fun c ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.WittVector.Isocrystal (goal)
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
F₀ : LinearMap.{u_2, u_2, u_2, u_3} (R := K(p, k)) (RingHom.id K(p, k)) (StandardOneDimIsocrystal p k m) V :=
  LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯
c : StandardOneDimIsocrystal p k m
⊢ Eq (α := V)
    ((Φ(p, k) : (a : V) → V)
        ((LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb ≪≫ₗ F :
              (a : StandardOneDimIsocrystal p k m) → V)
            c :
          V) :
      V)
    ((LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb ≪≫ₗ F :
          (a : StandardOneDimIsocrystal p k m) → V)
        ((Φ(p, k) : (a : StandardOneDimIsocrystal p k m) → StandardOneDimIsocrystal p k m) c :
          StandardOneDimIsocrystal p k m) :
      V)
have h : (Φ(p, k) : (a : V) → V) (HSMul.hSMul (β := V) b ((F₀ : (a : StandardOneDimIsocrystal p k m) → V) c : V)) =
  HSMul.hSMul (β := V) b
    ((F₀ : (a : StandardOneDimIsocrystal p k m) → V)
        (HSMul.hSMul (β := K(p, k)) (HPow.hPow (α := K(p, k)) (↑p : K(p, k)) m)
          ((φ(p, k) : (a : K(p, k)) → K(p, k)) c : K(p, k))) :
      V)
Tactic: rw [LinearEquiv.trans_apply, LinearEquiv.trans_apply, LinearEquiv.smulOfNeZero_apply,
    LinearEquiv.smulOfNeZero_apply, LinearEquiv.map_smul, LinearEquiv.map_smul,
    LinearEquiv.ofBijective_apply, LinearEquiv.ofBijective_apply,
    StandardOneDimIsocrystal.frobenius_apply]