-- Mathlib/RingTheory/Perfection.lean
theorem map_eq_zero {f : PreTilt O p} : val K v O hv p f = 0 ↔ f = 0

Proof state:
case neg
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
hf0 : ¬f = 0
⊢ (val K v O hv p) f = 0 ↔ f = 0

Tactic:
obtain ⟨n, hn⟩ : ∃ n, coeff _ _ n f ≠ 0 := not_forall.1 fun h => hf0 <| Perfection.ext h

Result:
case neg.intro
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
hf0 : ¬f = 0
n : ℕ
hn : (coeff (ModP O p) p n) f ≠ 0
⊢ (val K v O hv p) f = 0 ↔ f = 0

Proof state:
case pos
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
hf0 : f = 0
⊢ (val K v O hv p) f = 0 ↔ f = 0

Tactic:
rw [hf0]

Result:
case pos
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
hf0 : f = 0
⊢ (val K v O hv p) 0 = 0 ↔ 0 = 0

Proof state:
case pos
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
hf0 : f = 0
⊢ (val K v O hv p) 0 = 0 ↔ 0 = 0

Tactic:
exact iff_of_true (Valuation.map_zero _) rfl

Result:
no goals

Proof state:
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
⊢ (val K v O hv p) f = 0 ↔ f = 0

Tactic:
by_cases hf0 : f = 0

Result:
case pos
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
hf0 : f = 0
⊢ (val K v O hv p) f = 0 ↔ f = 0

case neg
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
hf0 : ¬f = 0
⊢ (val K v O hv p) f = 0 ↔ f = 0

Proof state:
case neg.intro
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
hf0 : ¬f = 0
n : ℕ
hn : (coeff (ModP O p) p n) f ≠ 0
⊢ (val K v O hv p) f = 0 ↔ f = 0

Tactic:
show valAux K v O p f = 0 ↔ f = 0

Result:
case neg.intro
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
hf0 : ¬f = 0
n : ℕ
hn : (coeff (ModP O p) p n) f ≠ 0
⊢ valAux K v O p f = 0 ↔ f = 0

Proof state:
case neg.intro
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
hf0 : ¬f = 0
n : ℕ
hn : (coeff (ModP O p) p n) f ≠ 0
hvf : ModP.preVal K v O p ((coeff (ModP O p) p n) f) = 0
⊢ (coeff (ModP O p) p n) f = 0

Tactic:
rwa [ModP.preVal_eq_zero hv] at hvf

Result:
no goals

Proof state:
case neg.intro
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
hf0 : ¬f = 0
n : ℕ
hn : (coeff (ModP O p) p n) f ≠ 0
hvf : ModP.preVal K v O p ((coeff (ModP O p) p n) f) ^ p ^ n = 0
⊢ (coeff (ModP O p) p n) f = 0

Tactic:
replace hvf := pow_eq_zero hvf

Result:
case neg.intro
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
hf0 : ¬f = 0
n : ℕ
hn : (coeff (ModP O p) p n) f ≠ 0
hvf : ModP.preVal K v O p ((coeff (ModP O p) p n) f) = 0
⊢ (coeff (ModP O p) p n) f = 0

Proof state:
case neg.intro
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
hf0 : ¬f = 0
n : ℕ
hn : (coeff (ModP O p) p n) f ≠ 0
⊢ valAux K v O p f = 0 ↔ f = 0

Tactic:
refine iff_of_false (fun hvf => hn ?_) hf0

Result:
case neg.intro
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
hf0 : ¬f = 0
n : ℕ
hn : (coeff (ModP O p) p n) f ≠ 0
hvf : valAux K v O p f = 0
⊢ (coeff (ModP O p) p n) f = 0

Proof state:
case neg.intro
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
hf0 : ¬f = 0
n : ℕ
hn : (coeff (ModP O p) p n) f ≠ 0
hvf : valAux K v O p f = 0
⊢ (coeff (ModP O p) p n) f = 0

Tactic:
rw [valAux_eq hv hn] at hvf

Result:
case neg.intro
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
hf0 : ¬f = 0
n : ℕ
hn : (coeff (ModP O p) p n) f ≠ 0
hvf : ModP.preVal K v O p ((coeff (ModP O p) p n) f) ^ p ^ n = 0
⊢ (coeff (ModP O p) p n) f = 0