awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
refine_2 :
  Function.Surjective.{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

Tactic:
refine LinearEquiv.ofBijective F₀ ⟨?_, ?_⟩

Premises used: And.intro, LinearEquiv.ofBijective
-- 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
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 : F₀.ker = ⊥
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := StandardOneDimIsocrystal p k m) (β := V)
    (⇑F₀ : (a : StandardOneDimIsocrystal p k m) → V)

Tactic:
rw [← LinearMap.ker_eq_bot]

Premises used: LinearMap.ker_eq_bot
-- 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
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₀.ker = ⊥

Tactic:
LinearMap.ker_toSpanSingleton K(p, k) hx

Premises used: WittVector.instAddCommGroupStandardOneDimIsocrystal._aux_1, FractionRing, LinearMap.ker_toSpanSingleton, WittVector.StandardOneDimIsocrystal, WittVector
-- 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
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₀.ker = ⊥

Tactic:
exact LinearMap.ker_toSpanSingleton K(p, k) hx

Premises used: FractionRing, LinearMap.ker_toSpanSingleton, WittVector
-- 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
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_2 : F₀.range = ⊤
⊢ Function.Surjective.{u_2 + 1, u_3 + 1} (α := StandardOneDimIsocrystal p k m) (β := V)
    (⇑F₀ : (a : StandardOneDimIsocrystal p k m) → V)

Tactic:
rw [← LinearMap.range_eq_top]

Premises used: LinearMap.range_eq_top
-- 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
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_2 : F₀.range = K(p, k) ∙ x
⊢ F₀.range = ⊤

Tactic:
rw [← (finrank_eq_one_iff_of_nonzero x hx).mp h_dim]

Premises used: Iff.mp, 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)
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_2 refine_2₁ : F₀.range = LinearMap.range (LinearMap.toSpanSingleton K(p, k) V x)
⊢ F₀.range = K(p, k) ∙ x

Tactic:
rw [LinearMap.span_singleton_eq_range]

Premises used: LinearMap.span_singleton_eq_range
-- 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
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)

Tactic:
⟨⟨(LinearEquiv.smulOfNeZero K(p, k) _ _ hb).trans F, fun c ↦ ?_⟩⟩

Premises used: WittVector.IsocrystalEquiv.mk, FractionRing, Nonempty.intro, WittVector, LinearEquiv.smulOfNeZero, LinearEquiv.trans
-- 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
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₀ ⋯
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)
⊢ Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)

Tactic:
refine ⟨⟨(LinearEquiv.smulOfNeZero K(p, k) _ _ hb).trans F, fun c ↦ ?_⟩⟩
-- 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
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
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)
⊢ 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:
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]

Premises used: LinearEquiv.trans_apply, LinearEquiv.ofBijective_apply, LinearEquiv.smulOfNeZero_apply, WittVector.StandardOneDimIsocrystal.frobenius_apply, LinearEquiv.map_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)
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
h :
  (Φ(p, k) : (a : V) → V) (HSMul.hSMul (β := V) b ((F₀ : (a : K(p, k)) → V) c : V)) =
    HSMul.hSMul (β := V) b
      ((F₀ : (a : K(p, k)) → 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)
⊢ (Φ(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:
unfold StandardOneDimIsocrystal

Premises used: WittVector.StandardOneDimIsocrystal
-- 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
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
h :
  (Φ(p, k) : (a : V) → V) (b • c • x) =
    b •
      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)) •
        x
⊢ (Φ(p, k) : (a : V) → V) (HSMul.hSMul (β := V) b ((F₀ : (a : K(p, k)) → V) c : V)) =
    HSMul.hSMul (β := V) b
      ((F₀ : (a : K(p, k)) → 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 [LinearMap.toSpanSingleton_apply K(p, k) V x c, LinearMap.toSpanSingleton_apply K(p, k) V x]

Premises used: FractionRing, LinearMap.toSpanSingleton_apply, WittVector
-- 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
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
h :
  HSMul.hSMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) b : K(p, k))
      (HSMul.hSMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) c : K(p, k)) (a • x)) =
    b •
      HMul.hMul (β := 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)) •
        x
⊢ (Φ(p, k) : (a : V) → V) (b • c • x) =
    b •
      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)) •
        x

Tactic:
simp only [hax, map_smulₛₗ, smul_eq_mul]

Premises used: MulActionSemiHomClass.map_smulₛₗ, smul_eq_mul
-- 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
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
h :
  HMul.hMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) b : K(p, k))
        (HMul.hMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) c : K(p, k)) a) •
      x =
    (b *
        HMul.hMul (β := 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))) •
      x
⊢ HSMul.hSMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) b : K(p, k))
      (HSMul.hSMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) c : K(p, k)) (a • x)) =
    b •
      HMul.hMul (β := 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)) •
        x

Tactic:
simp only [← mul_smul]

Premises used: SemigroupAction.mul_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)
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
h :
  HMul.hMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) b : K(p, k))
      (HMul.hMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) c : K(p, k)) a) =
    b *
      HMul.hMul (β := 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))
⊢ HMul.hMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) b : K(p, k))
        (HMul.hMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) c : K(p, k)) a) •
      x =
    (b *
        HMul.hMul (β := 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))) •
      x

Tactic:
congr 1
-- 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
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
⊢ HMul.hMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) b : K(p, k))
      (HMul.hMul (α := K(p, k)) ((φ(p, k) : (a : K(p, k)) → K(p, k)) c : K(p, k)) a) =
    b *
      HMul.hMul (β := 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))

Tactic:
linear_combination φ(p, k) c * hmb

Premises used: WittVector.FractionRing.frobeniusRingHom, DFunLike.coe
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
apply :
  vars (R := ℤ) ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n)) ∪
      vars (R := ℤ) ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n)) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
⊢ (HMul.hMul (α := 𝕄) (β := 𝕄) ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n) : 𝕄)
        ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n) : 𝕄)).vars ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
apply Subset.trans (vars_mul _ _)

Premises used: Finset.Subset.trans, MvPolynomial.vars_mul
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ vars (R := ℤ) ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n)) ∪
      vars (R := ℤ) ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n)) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
union_subset ?_ ?_

Premises used: Finset.union_subset
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
refine_1 :
  vars (R := ℤ) ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n)) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
refine_2 :
  vars (R := ℤ) ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n)) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
⊢ vars (R := ℤ) ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n)) ∪
      vars (R := ℤ) ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n)) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
refine union_subset ?_ ?_

Premises used: Finset.union_subset
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ vars (R := ℤ) ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n)) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
Subset.trans (vars_rename _ _) ?_

Premises used: Finset.Subset.trans, MvPolynomial.vars_rename
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
refine_1 : image (Prod.mk 0) (vars (wittPolynomial p ℤ n)) ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))
⊢ vars (R := ℤ) ((rename (Prod.mk 0) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n)) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
refine Subset.trans (vars_rename _ _) ?_

Premises used: Finset.Subset.trans, MvPolynomial.vars_rename
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ image (Prod.mk 0) (vars (wittPolynomial p ℤ n)) ⊆ SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
simp [wittPolynomial_vars, image_subset_iff]

Premises used: wittPolynomial_vars, Finset.image_subset_iff
-- Module: Mathlib.RingTheory.WittVector.MulCoeff
Goal:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ vars (R := ℤ) ((rename (Prod.mk 1) : (a : MvPolynomial ℕ ℤ) → 𝕄) (wittPolynomial p ℤ n)) ⊆
    SProd.sprod (α := Finset (Fin 2)) univ (range (n + 1))

Tactic:
Subset.trans (vars_rename _ _) ?_

Premises used: Finset.Subset.trans, MvPolynomial.vars_rename