[GOAL]
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
k : Type u_1
inst✝³ : CommRing k
inst✝² : IsDomain k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
m : ℤ
x : StandardOneDimIsocrystal p k m
⊢ ↑Φ(p, k) x = ↑p ^ m • ↑φ(p, k) x
[PROOFSTEP]
erw [smul_eq_mul]
[GOAL]
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
k : Type u_1
inst✝³ : CommRing k
inst✝² : IsDomain k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
m : ℤ
x : StandardOneDimIsocrystal p k m
⊢ ↑Φ(p, k) x =
    ↑(IsFractionRing.lift (_ : Function.Injective ↑(algebraMap (WittVector p k) ((fun x => K(p, k)) x)))) (↑p ^ m) *
      ↑φ(p, k) x
[PROOFSTEP]
simp only [map_zpow₀, map_natCast]
[GOAL]
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
k : Type u_1
inst✝³ : CommRing k
inst✝² : IsDomain k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
m : ℤ
x : StandardOneDimIsocrystal p k m
⊢ ↑Φ(p, k) x = ↑p ^ m * ↑φ(p, k) x
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
⊢ ∃ m, Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
[PROOFSTEP]
haveI : Nontrivial V := FiniteDimensional.nontrivial_of_finrank_eq_succ h_dim
[GOAL]
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this : Nontrivial V
⊢ ∃ m, Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
[PROOFSTEP]
obtain ⟨x, hx⟩ : ∃ x : V, x ≠ 0 := exists_ne 0
[GOAL]
case intro
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ ∃ m, Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
[PROOFSTEP]
have : Φ(p, k) x ≠ 0 := by simpa only [map_zero] using Φ(p, k).injective.ne hx
[GOAL]
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ ↑Φ(p, k) x ≠ 0
[PROOFSTEP]
simpa only [map_zero] using Φ(p, k).injective.ne hx
[GOAL]
case intro
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
⊢ ∃ m, Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
[PROOFSTEP]
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]
[GOAL]
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
⊢ ∃ a, a ≠ 0 ∧ ↑Φ(p, k) x = a • x
[PROOFSTEP]
rw [finrank_eq_one_iff_of_nonzero' x hx] at h_dim
[GOAL]
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
this✝ : Nontrivial V
x : V
h_dim : ∀ (w : V), ∃ c, c • x = w
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
⊢ ∃ a, a ≠ 0 ∧ ↑Φ(p, k) x = a • x
[PROOFSTEP]
obtain ⟨a, ha⟩ := h_dim (Φ(p, k) x)
[GOAL]
case intro
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
this✝ : Nontrivial V
x : V
h_dim : ∀ (w : V), ∃ c, c • x = w
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a • x = ↑Φ(p, k) x
⊢ ∃ a, a ≠ 0 ∧ ↑Φ(p, k) x = a • x
[PROOFSTEP]
refine' ⟨a, _, ha.symm⟩
[GOAL]
case intro
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
this✝ : Nontrivial V
x : V
h_dim : ∀ (w : V), ∃ c, c • x = w
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a • x = ↑Φ(p, k) x
⊢ a ≠ 0
[PROOFSTEP]
intro ha'
[GOAL]
case intro
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
this✝ : Nontrivial V
x : V
h_dim : ∀ (w : V), ∃ c, c • x = w
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a • x = ↑Φ(p, k) x
ha' : a = 0
⊢ False
[PROOFSTEP]
apply this
[GOAL]
case intro
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
this✝ : Nontrivial V
x : V
h_dim : ∀ (w : V), ∃ c, c • x = w
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a • x = ↑Φ(p, k) x
ha' : a = 0
⊢ ↑Φ(p, k) x = 0
[PROOFSTEP]
simp only [← ha, ha', zero_smul]
[GOAL]
case intro.intro.intro
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
⊢ ∃ m, Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
[PROOFSTEP]
obtain ⟨b, hb, m, hmb⟩ := WittVector.exists_frobenius_solution_fractionRing p ha
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : ↑(IsFractionRing.fieldEquivOfRingEquiv (frobeniusEquiv p k)) b * a = ↑p ^ m * b
⊢ ∃ m, Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
[PROOFSTEP]
replace hmb : φ(p, k) b * a = (p : K(p, k)) ^ m * b := by convert hmb
[GOAL]
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : ↑(IsFractionRing.fieldEquivOfRingEquiv (frobeniusEquiv p k)) b * a = ↑p ^ m * b
⊢ ↑φ(p, k) b * a = ↑p ^ m * b
[PROOFSTEP]
convert hmb
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : ↑φ(p, k) b * a = ↑p ^ m * b
⊢ ∃ m, Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
[PROOFSTEP]
use m
[GOAL]
case h
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : ↑φ(p, k) b * a = ↑p ^ m * b
⊢ Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
[PROOFSTEP]
let F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
[GOAL]
case h
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : ↑φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
⊢ Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
[PROOFSTEP]
let F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  by
  refine' LinearEquiv.ofBijective F₀ ⟨_, _⟩
  · rw [← LinearMap.ker_eq_bot]
    exact LinearMap.ker_toSpanSingleton K(p, k) V hx
  · rw [← LinearMap.range_eq_top]
    rw [← (finrank_eq_one_iff_of_nonzero x hx).mp h_dim]
    rw [LinearMap.span_singleton_eq_range]
      -- Porting note: `refine'` below gets confused when this is inlined.
[GOAL]
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : ↑φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
⊢ StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V
[PROOFSTEP]
refine' LinearEquiv.ofBijective F₀ ⟨_, _⟩
[GOAL]
case refine'_1
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : ↑φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
⊢ Function.Injective ↑F₀
[PROOFSTEP]
rw [← LinearMap.ker_eq_bot]
[GOAL]
case refine'_1
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : ↑φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
⊢ LinearMap.ker F₀ = ⊥
[PROOFSTEP]
exact LinearMap.ker_toSpanSingleton K(p, k) V hx
[GOAL]
case refine'_2
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : ↑φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
⊢ Function.Surjective ↑F₀
[PROOFSTEP]
rw [← LinearMap.range_eq_top]
[GOAL]
case refine'_2
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : ↑φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
⊢ LinearMap.range F₀ = ⊤
[PROOFSTEP]
rw [← (finrank_eq_one_iff_of_nonzero x hx).mp h_dim]
[GOAL]
case refine'_2
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : ↑φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
⊢ LinearMap.range F₀ = Submodule.span K(p, k) {x}
[PROOFSTEP]
rw [LinearMap.span_singleton_eq_range]
  -- Porting note: `refine'` below gets confused when this is inlined.
[GOAL]
case h
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : ↑φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.ofBijective F₀ (_ : Function.Injective ↑F₀ ∧ Function.Surjective ↑F₀)
⊢ Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
[PROOFSTEP]
let E := (LinearEquiv.smulOfNeZero K(p, k) _ _ hb).trans F
[GOAL]
case h
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : ↑φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.ofBijective F₀ (_ : Function.Injective ↑F₀ ∧ Function.Surjective ↑F₀)
E : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.trans (LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb) F
⊢ Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
[PROOFSTEP]
refine' ⟨⟨E, _⟩⟩
[GOAL]
case h
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : ↑φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.ofBijective F₀ (_ : Function.Injective ↑F₀ ∧ Function.Surjective ↑F₀)
E : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.trans (LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb) F
⊢ ∀ (x : StandardOneDimIsocrystal p k m), ↑Φ(p, k) (↑E x) = ↑E (↑Φ(p, k) x)
[PROOFSTEP]
simp only
[GOAL]
case h
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : ↑φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.ofBijective F₀ (_ : Function.Injective ↑F₀ ∧ Function.Surjective ↑F₀)
E : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.trans (LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb) F
⊢ ∀ (x_1 : StandardOneDimIsocrystal p k m),
    ↑Φ(p, k)
        (↑(LinearEquiv.trans (LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb)
              (LinearEquiv.ofBijective (LinearMap.toSpanSingleton K(p, k) V x)
                (_ : Function.Injective ↑F₀ ∧ Function.Surjective ↑F₀)))
          x_1) =
      ↑(LinearEquiv.trans (LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb)
            (LinearEquiv.ofBijective (LinearMap.toSpanSingleton K(p, k) V x)
              (_ : Function.Injective ↑F₀ ∧ Function.Surjective ↑F₀)))
        (↑Φ(p, k) x_1)
[PROOFSTEP]
intro c
[GOAL]
case h
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : ↑φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.ofBijective F₀ (_ : Function.Injective ↑F₀ ∧ Function.Surjective ↑F₀)
E : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.trans (LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb) F
c : StandardOneDimIsocrystal p k m
⊢ ↑Φ(p, k)
      (↑(LinearEquiv.trans (LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb)
            (LinearEquiv.ofBijective (LinearMap.toSpanSingleton K(p, k) V x)
              (_ : Function.Injective ↑F₀ ∧ Function.Surjective ↑F₀)))
        c) =
    ↑(LinearEquiv.trans (LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb)
          (LinearEquiv.ofBijective (LinearMap.toSpanSingleton K(p, k) V x)
            (_ : Function.Injective ↑F₀ ∧ Function.Surjective ↑F₀)))
      (↑Φ(p, k) c)
[PROOFSTEP]
rw [LinearEquiv.trans_apply, LinearEquiv.trans_apply, LinearEquiv.smulOfNeZero_apply, LinearEquiv.smulOfNeZero_apply,
  LinearEquiv.map_smul, LinearEquiv.map_smul]
  -- Porting note: was
    -- simp only [hax, LinearEquiv.ofBijective_apply, LinearMap.toSpanSingleton_apply,
    --   LinearEquiv.map_smulₛₗ, StandardOneDimIsocrystal.frobenius_apply, Algebra.id.smul_eq_mul]
[GOAL]
case h
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : ↑φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.ofBijective F₀ (_ : Function.Injective ↑F₀ ∧ Function.Surjective ↑F₀)
E : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.trans (LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb) F
c : StandardOneDimIsocrystal p k m
⊢ ↑Φ(p, k)
      (b •
        ↑(LinearEquiv.ofBijective (LinearMap.toSpanSingleton K(p, k) V x)
              (_ : Function.Injective ↑F₀ ∧ Function.Surjective ↑F₀))
          c) =
    b •
      ↑(LinearEquiv.ofBijective (LinearMap.toSpanSingleton K(p, k) V x)
            (_ : Function.Injective ↑F₀ ∧ Function.Surjective ↑F₀))
        (↑Φ(p, k) c)
[PROOFSTEP]
rw [LinearEquiv.ofBijective_apply, LinearEquiv.ofBijective_apply]
[GOAL]
case h
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : ↑φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.ofBijective F₀ (_ : Function.Injective ↑F₀ ∧ Function.Surjective ↑F₀)
E : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.trans (LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb) F
c : StandardOneDimIsocrystal p k m
⊢ ↑Φ(p, k) (b • ↑(LinearMap.toSpanSingleton K(p, k) V x) c) = b • ↑(LinearMap.toSpanSingleton K(p, k) V x) (↑Φ(p, k) c)
[PROOFSTEP]
erw [LinearMap.toSpanSingleton_apply K(p, k) V x c, LinearMap.toSpanSingleton_apply K(p, k) V x]
[GOAL]
case h
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : ↑φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.ofBijective F₀ (_ : Function.Injective ↑F₀ ∧ Function.Surjective ↑F₀)
E : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.trans (LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb) F
c : StandardOneDimIsocrystal p k m
⊢ ↑Φ(p, k) (b • c • x) = b • ↑Φ(p, k) c • x
[PROOFSTEP]
simp only [hax, LinearEquiv.ofBijective_apply, LinearMap.toSpanSingleton_apply, LinearEquiv.map_smulₛₗ,
  StandardOneDimIsocrystal.frobenius_apply, Algebra.id.smul_eq_mul]
[GOAL]
case h
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : ↑φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.ofBijective F₀ (_ : Function.Injective ↑F₀ ∧ Function.Surjective ↑F₀)
E : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.trans (LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb) F
c : StandardOneDimIsocrystal p k m
⊢ ↑φ(p, k) b • ↑φ(p, k) c • a • x = b • (↑p ^ m • ↑φ(p, k) c) • x
[PROOFSTEP]
simp only [← mul_smul]
[GOAL]
case h
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : ↑φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.ofBijective F₀ (_ : Function.Injective ↑F₀ ∧ Function.Surjective ↑F₀)
E : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.trans (LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb) F
c : StandardOneDimIsocrystal p k m
⊢ (↑φ(p, k) b * (↑φ(p, k) c * a)) • x = (b * ↑p ^ m • ↑φ(p, k) c) • x
[PROOFSTEP]
congr 1
  -- Porting note: added the next two lines
[GOAL]
case h.e_a
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : ↑φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.ofBijective F₀ (_ : Function.Injective ↑F₀ ∧ Function.Surjective ↑F₀)
E : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.trans (LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb) F
c : StandardOneDimIsocrystal p k m
⊢ ↑φ(p, k) b * (↑φ(p, k) c * a) = b * ↑p ^ m • ↑φ(p, k) c
[PROOFSTEP]
erw [smul_eq_mul]
[GOAL]
case h.e_a
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : ↑φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.ofBijective F₀ (_ : Function.Injective ↑F₀ ∧ Function.Surjective ↑F₀)
E : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.trans (LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb) F
c : StandardOneDimIsocrystal p k m
⊢ ↑φ(p, k) b * (↑φ(p, k) c * a) =
    b *
      (↑(IsFractionRing.lift (_ : Function.Injective ↑(algebraMap (WittVector p k) ((fun x => K(p, k)) c)))) (↑p ^ m) *
        ↑φ(p, k) c)
[PROOFSTEP]
simp only [map_zpow₀, map_natCast]
[GOAL]
case h.e_a
p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
k✝ : Type u_1
inst✝⁵ : CommRing k✝
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : ↑Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : ↑Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : ↑φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.ofBijective F₀ (_ : Function.Injective ↑F₀ ∧ Function.Surjective ↑F₀)
E : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V :=
  LinearEquiv.trans (LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb) F
c : StandardOneDimIsocrystal p k m
⊢ ↑φ(p, k) b * (↑φ(p, k) c * a) = b * (↑p ^ m * ↑φ(p, k) c)
[PROOFSTEP]
linear_combination φ(p, k) c * hmb