-- Mathlib/ModelTheory/Algebra/Field/CharP.lean
theorem charP_iff_model_fieldOfChar [Field K] [CompatibleRing K] :
    (Theory.fieldOfChar p).Model K ↔ CharP K p

Proof state:
case pos
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : p = 0
⊢ K ⊨ (fun q => ∼(eqZero q)) '' {q | Nat.Prime q} ↔ CharP K p

Tactic:
subst hp0

Result:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ K ⊨ (fun q => ∼(eqZero q)) '' {q | Nat.Prime q} ↔ CharP K 0

Proof state:
case pos
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : ¬p = 0
hp : Nat.Prime p
⊢ K ⊨ {eqZero p} ↔ CharP K p

Tactic:
simp only [Theory.model_iff, Set.mem_singleton_iff, Sentence.Realize, forall_eq,
  realize_eqZero, ← CharP.charP_iff_prime_eq_zero hp]

Result:
no goals

Proof state:
case neg
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : ¬p = 0
hp : ¬Nat.Prime p
⊢ K ⊨ {⊥} ↔ CharP K p

Tactic:
simp only [Theory.model_iff, Set.mem_singleton_iff, Sentence.Realize,
  forall_eq, Formula.realize_bot, false_iff]

Result:
case neg
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : ¬p = 0
hp : ¬Nat.Prime p
⊢ ¬CharP K p

Proof state:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ K ⊨ (fun q => ∼(eqZero q)) '' {q | Nat.Prime q} ↔ CharP K 0

Tactic:
simp only [Theory.model_iff, Set.mem_image, Set.mem_setOf_eq, Sentence.Realize,
  forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, Formula.realize_not,
  realize_eqZero, ← CharZero.charZero_iff_forall_prime_ne_zero]

Result:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ CharZero K ↔ CharP K 0

Proof state:
case neg
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : ¬p = 0
hp : ¬Nat.Prime p
H : CharP K p
⊢ False

Tactic:
cases (CharP.char_is_prime_or_zero K p) <;> simp_all

Result:
no goals

Proof state:
case neg
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : ¬p = 0
hp : ¬Nat.Prime p
⊢ ¬CharP K p

Tactic:
intro H

Result:
case neg
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : ¬p = 0
hp : ¬Nat.Prime p
H : CharP K p
⊢ False

Proof state:
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ K ⊨ Theory.field

Tactic:
infer_instance

Result:
no goals

Proof state:
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ (K ⊨ if p = 0 then (fun q => ∼(eqZero q)) '' {q | Nat.Prime q} else if Nat.Prime p then {eqZero p} else {⊥}) ↔
    CharP K p

Tactic:
split_ifs with hp0 hp

Result:
case pos
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : p = 0
⊢ K ⊨ (fun q => ∼(eqZero q)) '' {q | Nat.Prime q} ↔ CharP K p

case pos
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : ¬p = 0
hp : Nat.Prime p
⊢ K ⊨ {eqZero p} ↔ CharP K p

case neg
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
hp0 : ¬p = 0
hp : ¬Nat.Prime p
⊢ K ⊨ {⊥} ↔ CharP K p

Proof state:
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ K ⊨ Theory.fieldOfChar p ↔ CharP K p

Tactic:
simp only [Theory.fieldOfChar, Theory.model_union_iff,
  (show (Theory.field.Model K) by infer_instance), true_and]

Result:
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ (K ⊨ if p = 0 then (fun q => ∼(eqZero q)) '' {q | Nat.Prime q} else if Nat.Prime p then {eqZero p} else {⊥}) ↔
    CharP K p

Proof state:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ CharZero K ↔ CharP K 0

Tactic:
exact ⟨fun _ => CharP.ofCharZero _, fun _ => CharP.charP_to_charZero K⟩

Result:
no goals