-- Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean
theorem exists_frobenius_solution_fractionRing {a : FractionRing (𝕎 k)} (ha : a ≠ 0) :
    ∃ᵉ (b ≠ 0) (m : ℤ), φ b * a = (p : FractionRing (𝕎 k)) ^ m * b

Proof state:
case mk.mk.intro.intro.intro.intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
m : ℕ
r' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hr0 : ↑p ^ m * r' ≠ 0
n : ℕ
q' : 𝕎 k
hq' : q'.coeff 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
hq0 : ↑p ^ n * q' ≠ 0
hrq : Localization.mk (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).1 (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).2 ≠ 0
b : 𝕎 k := frobeniusRotation p hr' hq'
⊢ ∃ b,
    b ≠ 0 ∧
      ∃ m_1, φ b * Localization.mk (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).1 (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).2 = ↑p ^ m_1 * b

Tactic:
refine ⟨algebraMap (𝕎 k) (FractionRing (𝕎 k)) b, ?_, m - n, ?_⟩

Result:
case mk.mk.intro.intro.intro.intro.intro.intro.refine_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
m : ℕ
r' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hr0 : ↑p ^ m * r' ≠ 0
n : ℕ
q' : 𝕎 k
hq' : q'.coeff 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
hq0 : ↑p ^ n * q' ≠ 0
hrq : Localization.mk (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).1 (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).2 ≠ 0
b : 𝕎 k := frobeniusRotation p hr' hq'
⊢ (algebraMap (𝕎 k) (FractionRing (𝕎 k))) b ≠ 0

case mk.mk.intro.intro.intro.intro.intro.intro.refine_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
m : ℕ
r' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hr0 : ↑p ^ m * r' ≠ 0
n : ℕ
q' : 𝕎 k
hq' : q'.coeff 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
hq0 : ↑p ^ n * q' ≠ 0
hrq : Localization.mk (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).1 (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).2 ≠ 0
b : 𝕎 k := frobeniusRotation p hr' hq'
⊢ φ ((algebraMap (𝕎 k) (FractionRing (𝕎 k))) b) *
      Localization.mk (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).1 (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).2 =
    ↑p ^ (↑m - ↑n) * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) b

Proof state:
case mk.mk
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
r q : 𝕎 k
hq : q ∈ nonZeroDivisors (𝕎 k)
hrq : Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 ≠ 0
hq0 : q ≠ 0
⊢ ∃ b, b ≠ 0 ∧ ∃ m, φ b * Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 = ↑p ^ m * b

Tactic:
have hr0 : r ≠ 0 := fun h => hrq (by simp [h])

Result:
case mk.mk
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
r q : 𝕎 k
hq : q ∈ nonZeroDivisors (𝕎 k)
hrq : Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 ≠ 0
hq0 : q ≠ 0
hr0 : r ≠ 0
⊢ ∃ b, b ≠ 0 ∧ ∃ m, φ b * Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 = ↑p ^ m * b

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
⊢ a ≠ 0 → ∃ b, b ≠ 0 ∧ ∃ m, φ b * a = ↑p ^ m * b

Tactic:
refine Localization.induction_on a ?_

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
⊢ ∀ (y : 𝕎 k × ↥(nonZeroDivisors (𝕎 k))),
    Localization.mk y.1 y.2 ≠ 0 → ∃ b, b ≠ 0 ∧ ∃ m, φ b * Localization.mk y.1 y.2 = ↑p ^ m * b

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
r q : 𝕎 k
hq : q ∈ nonZeroDivisors (𝕎 k)
hrq : Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 ≠ 0
hq0 : q ≠ 0
h : r = 0
⊢ Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 = 0

Tactic:
simp [h]

Result:
no goals

Proof state:
case mk.mk
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
r q : 𝕎 k
hq : q ∈ nonZeroDivisors (𝕎 k)
hrq : Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 ≠ 0
⊢ ∃ b, b ≠ 0 ∧ ∃ m, φ b * Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 = ↑p ^ m * b

Tactic:
have hq0 : q ≠ 0 := mem_nonZeroDivisors_iff_ne_zero.1 hq

Result:
case mk.mk
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
r q : 𝕎 k
hq : q ∈ nonZeroDivisors (𝕎 k)
hrq : Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 ≠ 0
hq0 : q ≠ 0
⊢ ∃ b, b ≠ 0 ∧ ∃ m, φ b * Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 = ↑p ^ m * b

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
ha : a ≠ 0
⊢ ∃ b, b ≠ 0 ∧ ∃ m, φ b * a = ↑p ^ m * b

Tactic:
revert ha

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
⊢ a ≠ 0 → ∃ b, b ≠ 0 ∧ ∃ m, φ b * a = ↑p ^ m * b

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
⊢ ∀ (y : 𝕎 k × ↥(nonZeroDivisors (𝕎 k))),
    Localization.mk y.1 y.2 ≠ 0 → ∃ b, b ≠ 0 ∧ ∃ m, φ b * Localization.mk y.1 y.2 = ↑p ^ m * b

Tactic:
rintro ⟨r, q, hq⟩ hrq

Result:
case mk.mk
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
r q : 𝕎 k
hq : q ∈ nonZeroDivisors (𝕎 k)
hrq : Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 ≠ 0
⊢ ∃ b, b ≠ 0 ∧ ∃ m, φ b * Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 = ↑p ^ m * b

Proof state:
case mk.mk.intro.intro.intro.intro.intro.intro.refine_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
m : ℕ
r' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hr0 : ↑p ^ m * r' ≠ 0
n : ℕ
q' : 𝕎 k
hq' : q'.coeff 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
hq0 : ↑p ^ n * q' ≠ 0
hrq : Localization.mk (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).1 (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).2 ≠ 0
b : 𝕎 k := frobeniusRotation p hr' hq'
⊢ φ ((algebraMap (𝕎 k) (FractionRing (𝕎 k))) b) *
      Localization.mk (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).1 (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).2 =
    ↑p ^ (↑m - ↑n) * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) b

Tactic:
exact exists_frobenius_solution_fractionRing_aux p m n r' q' hr' hq' hq

Result:
no goals

Proof state:
case mk.mk
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
r q : 𝕎 k
hq : q ∈ nonZeroDivisors (𝕎 k)
hrq : Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 ≠ 0
hq0 : q ≠ 0
hr0 : r ≠ 0
⊢ ∃ b, b ≠ 0 ∧ ∃ m, φ b * Localization.mk (r, ⟨q, hq⟩).1 (r, ⟨q, hq⟩).2 = ↑p ^ m * b

Tactic:
obtain ⟨m, r', hr', rfl⟩ := exists_eq_pow_p_mul r hr0

Result:
case mk.mk.intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
q : 𝕎 k
hq : q ∈ nonZeroDivisors (𝕎 k)
hq0 : q ≠ 0
m : ℕ
r' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hrq : Localization.mk (↑p ^ m * r', ⟨q, hq⟩).1 (↑p ^ m * r', ⟨q, hq⟩).2 ≠ 0
hr0 : ↑p ^ m * r' ≠ 0
⊢ ∃ b, b ≠ 0 ∧ ∃ m_1, φ b * Localization.mk (↑p ^ m * r', ⟨q, hq⟩).1 (↑p ^ m * r', ⟨q, hq⟩).2 = ↑p ^ m_1 * b