internlm/Lean-Github huggingface dataset:
Theorem: Model.val_discr_of_val_ai
Proof state before:
case ha.hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ 12 ≤ v evr.valtn (-(27 * b6 e * b6 e))

case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ 12 ≤ v evr.valtn (9 * b2 e * b4 e * b6 e)
Tactic:
. rw [val_neg, mul_assoc]
  apply val_mul_ge_of_right_ge _ (val_mul_ge_of_both_ge _ hb6 hb6)
Proof state after:
case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ 12 ≤ v evr.valtn (9 * b2 e * b4 e * b6 e)
Theorem: Model.val_discr_of_val_ai
Proof state before:
case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ 12 ≤ v evr.valtn (9 * b2 e * b4 e * b6 e)
Tactic:
. rw [mul_assoc, mul_assoc]
  apply val_mul_ge_of_right_ge _ (val_mul_ge_of_both_ge _ hb2 (val_mul_ge_of_both_ge _ hb4 hb6))
Proof state after:
no goals
Theorem: Model.val_discr_of_val_ai
Proof state before:
case ha.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ 12 ≤ v evr.valtn (-b2 e * b2 e * b8 e + -(8 * b4 e ^ 3))
Tactic:
apply val_add_ge_of_ge
Proof state after:
case ha.ha.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ 12 ≤ v evr.valtn (-b2 e * b2 e * b8 e)

case ha.ha.hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ 12 ≤ v evr.valtn (-(8 * b4 e ^ 3))
Theorem: Model.val_discr_of_val_ai
Proof state before:
case ha.ha.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ 12 ≤ v evr.valtn (-b2 e * b2 e * b8 e)
Tactic:
rw [←neg_mul_eq_neg_mul, ←neg_mul_eq_neg_mul, val_neg]
Proof state after:
case ha.ha.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ 12 ≤ v evr.valtn (b2 e * b2 e * b8 e)
Theorem: Model.val_discr_of_val_ai
Proof state before:
case ha.ha.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ 12 ≤ v evr.valtn (b2 e * b2 e * b8 e)
Tactic:
apply val_mul_ge_of_both_ge _ (val_mul_ge_of_both_ge _ hb2 hb2) hb8
Proof state after:
no goals
Theorem: Model.val_discr_of_val_ai
Proof state before:
case ha.ha.hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ 12 ≤ v evr.valtn (-(8 * b4 e ^ 3))
Tactic:
rw [val_neg, pow_succ', pow_succ', pow_one]
Proof state after:
case ha.ha.hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ 12 ≤ v evr.valtn (8 * (b4 e * b4 e * b4 e))
Theorem: Model.val_discr_of_val_ai
Proof state before:
case ha.ha.hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ 12 ≤ v evr.valtn (8 * (b4 e * b4 e * b4 e))
Tactic:
apply val_mul_ge_of_right_ge _ (val_mul_ge_of_both_ge _ (val_mul_ge_of_both_ge _ hb4 hb4) hb4)
Proof state after:
no goals
Theorem: Model.val_discr_of_val_ai
Proof state before:
case ha.hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ 12 ≤ v evr.valtn (-(27 * b6 e * b6 e))
Tactic:
rw [val_neg, mul_assoc]
Proof state after:
case ha.hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ 12 ≤ v evr.valtn (27 * (b6 e * b6 e))
Theorem: Model.val_discr_of_val_ai
Proof state before:
case ha.hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ 12 ≤ v evr.valtn (27 * (b6 e * b6 e))
Tactic:
apply val_mul_ge_of_right_ge _ (val_mul_ge_of_both_ge _ hb6 hb6)
Proof state after:
no goals
Theorem: Model.val_discr_of_val_ai
Proof state before:
case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ 12 ≤ v evr.valtn (9 * b2 e * b4 e * b6 e)
Tactic:
rw [mul_assoc, mul_assoc]
Proof state after:
case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ 12 ≤ v evr.valtn (9 * (b2 e * (b4 e * b6 e)))
Theorem: Model.val_discr_of_val_ai
Proof state before:
case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ 12 ≤ v evr.valtn (9 * (b2 e * (b4 e * b6 e)))
Tactic:
apply val_mul_ge_of_right_ge _ (val_mul_ge_of_both_ge _ hb2 (val_mul_ge_of_both_ge _ hb4 hb6))
Proof state after:
no goals
Theorem: ValidModel.iso_rst_val_discr_to_nat
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
r s t : R
e : ValidModel R
⊢ val_discr_to_nat valp (rst_iso r s t e) = val_discr_to_nat valp e
Tactic:
simp [val_discr_to_nat]
Proof state after:
no goals
Theorem: ValidModel.ofN_val_discr_to_nat
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
e : ValidModel R
⊢ ↑(val_discr_to_nat valp e) = v valp (Model.discr e.toModel)
Tactic:
simp only [val_discr_to_nat, coe_toNat_eq_self, ne_eq, v_eq_top_iff_zero]
Proof state after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
e : ValidModel R
⊢ ¬Model.discr e.toModel = 0
Theorem: ValidModel.ofN_val_discr_to_nat
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
e : ValidModel R
⊢ ¬Model.discr e.toModel = 0
Tactic:
exact e.discr_not_zero
Proof state after:
no goals
Theorem: ValidModel.pi_scaling_val_discr_to_nat
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : ValidModel R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ val_discr_to_nat evr.valtn (pi_scaling evr e h1 h2 h3 h4 h6) = val_discr_to_nat evr.valtn e - 12
Tactic:
apply_fun (Nat.cast : ℕ → ℕ∞) using Nat.cast_injective (R := ℕ∞)
Proof state after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : ValidModel R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(val_discr_to_nat evr.valtn (pi_scaling evr e h1 h2 h3 h4 h6)) = ↑(val_discr_to_nat evr.valtn e - 12)
Theorem: ValidModel.pi_scaling_val_discr_to_nat
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : ValidModel R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(val_discr_to_nat evr.valtn (pi_scaling evr e h1 h2 h3 h4 h6)) = ↑(val_discr_to_nat evr.valtn e - 12)
Tactic:
rw [ofN_val_discr_to_nat, pi_scaling_toModel evr e h1 h2 h3 h4 h6,
  Model.discr_of_pi_scaling _ _ h1 h2 h3 h4 h6, evr.val_sub_val_eq]
Proof state after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : ValidModel R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑?m - ↑12 = ↑(val_discr_to_nat evr.valtn e - 12)

case m
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : ValidModel R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ ℕ

case h
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : ValidModel R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ v evr.valtn (Model.discr e.toModel) = ↑?m
Theorem: ValidModel.pi_scaling_val_discr_to_nat
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : ValidModel R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑?m - ↑12 = ↑(val_discr_to_nat evr.valtn e - 12)

case m
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : ValidModel R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ ℕ

case h
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : ValidModel R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ v evr.valtn (Model.discr e.toModel) = ↑?m
Tactic:
norm_cast
Proof state after:
case h
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : ValidModel R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ v evr.valtn (Model.discr e.toModel) = ↑(val_discr_to_nat evr.valtn e)
Theorem: ValidModel.pi_scaling_val_discr_to_nat
Proof state before:
case h
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : ValidModel R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ v evr.valtn (Model.discr e.toModel) = ↑(val_discr_to_nat evr.valtn e)
Tactic:
rw [ofN_val_discr_to_nat]
Proof state after:
no goals
Theorem: ValidModel.v_b4_of_v_a1_a3_a4
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
q : ℕ∞
p : R
valp : SurjVal p
e : ValidModel R
h1 : v valp e.a1 ≥ 1
h3 : v valp e.a3 ≥ q
h4 : v valp e.a4 ≥ q + 1
⊢ v valp (Model.b4 e.toModel) ≥ q + 1
Tactic:
apply val_add_ge_of_ge valp <;>
. simp
  elinarith
Proof state after:
no goals
Theorem: ValidModel.v_b4_of_v_a1_a3_a4
Proof state before:
case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
q : ℕ∞
p : R
valp : SurjVal p
e : ValidModel R
h1 : v valp e.a1 ≥ 1
h3 : v valp e.a3 ≥ q
h4 : v valp e.a4 ≥ q + 1
⊢ q + 1 ≤ v valp (2 * e.a4)
Tactic:
simp
Proof state after:
case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
q : ℕ∞
p : R
valp : SurjVal p
e : ValidModel R
h1 : v valp e.a1 ≥ 1
h3 : v valp e.a3 ≥ q
h4 : v valp e.a4 ≥ q + 1
⊢ q + 1 ≤ v valp 2 + v valp e.a4
Theorem: ValidModel.v_b4_of_v_a1_a3_a4
Proof state before:
case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
q : ℕ∞
p : R
valp : SurjVal p
e : ValidModel R
h1 : v valp e.a1 ≥ 1
h3 : v valp e.a3 ≥ q
h4 : v valp e.a4 ≥ q + 1
⊢ q + 1 ≤ v valp 2 + v valp e.a4
Tactic:
elinarith
Proof state after:
no goals
Theorem: ValidModel.v_b6_of_v_a3_a6
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
h3 : v valp e.a3 ≥ ↑q
h6 : v valp e.a6 ≥ 2 * ↑q
⊢ v valp (Model.b6 e.toModel) ≥ 2 * ↑q
Tactic:
apply val_add_ge_of_ge valp <;>
. simp
  elinarith
Proof state after:
no goals
Theorem: ValidModel.v_b6_of_v_a3_a6
Proof state before:
case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
h3 : v valp e.a3 ≥ ↑q
h6 : v valp e.a6 ≥ 2 * ↑q
⊢ 2 * ↑q ≤ v valp (4 * e.a6)
Tactic:
simp
Proof state after:
case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
h3 : v valp e.a3 ≥ ↑q
h6 : v valp e.a6 ≥ 2 * ↑q
⊢ 2 * ↑q ≤ v valp 4 + v valp e.a6
Theorem: ValidModel.v_b6_of_v_a3_a6
Proof state before:
case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
h3 : v valp e.a3 ≥ ↑q
h6 : v valp e.a6 ≥ 2 * ↑q
⊢ 2 * ↑q ≤ v valp 4 + v valp e.a6
Tactic:
elinarith
Proof state after:
no goals
Theorem: ValidModel.v_b8_of_v_ai
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
h1 : v valp e.a1 ≥ 1
h2 : v valp e.a2 = 1
h3 : v valp e.a3 ≥ ↑q
h4 : v valp e.a4 ≥ ↑q + 1
h6 : v valp e.a6 ≥ 2 * ↑q
⊢ v valp (Model.b8 e.toModel) ≥ 2 * ↑q + 1
Tactic:
apply_rules [val_add_ge_of_ge, val_sub_ge_of_ge] <;>
. simp
  elinarith
Proof state after:
no goals
Theorem: ValidModel.v_b8_of_v_ai
Proof state before:
case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
h1 : v valp e.a1 ≥ 1
h2 : v valp e.a2 = 1
h3 : v valp e.a3 ≥ ↑q
h4 : v valp e.a4 ≥ ↑q + 1
h6 : v valp e.a6 ≥ 2 * ↑q
h2_symm : 1 = v valp e.a2
⊢ 2 * ↑q + 1 ≤ v valp (e.a4 * e.a4)
Tactic:
simp
Proof state after:
case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
h1 : v valp e.a1 ≥ 1
h2 : v valp e.a2 = 1
h3 : v valp e.a3 ≥ ↑q
h4 : v valp e.a4 ≥ ↑q + 1
h6 : v valp e.a6 ≥ 2 * ↑q
h2_symm : 1 = v valp e.a2
⊢ 2 * ↑q + 1 ≤ v valp e.a4 + v valp e.a4
Theorem: ValidModel.v_b8_of_v_ai
Proof state before:
case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
h1 : v valp e.a1 ≥ 1
h2 : v valp e.a2 = 1
h3 : v valp e.a3 ≥ ↑q
h4 : v valp e.a4 ≥ ↑q + 1
h6 : v valp e.a6 ≥ 2 * ↑q
h2_symm : 1 = v valp e.a2
⊢ 2 * ↑q + 1 ≤ v valp e.a4 + v valp e.a4
Tactic:
elinarith
Proof state after:
no goals
Theorem: ValidModel.v_discr_of_v_ai
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
hq : q > 1
h1 : v valp e.a1 ≥ 1
h2 : v valp e.a2 = 1
h3 : v valp e.a3 ≥ ↑q
h4 : v valp e.a4 ≥ ↑q + 1
h6 : v valp e.a6 ≥ 2 * ↑q
⊢ v valp (Model.discr e.toModel) ≥ 2 * ↑q + 3
Tactic:
have h2' : valp e.b2 ≥ 1 := v_b2_of_v_a1_a2 valp e h1 h2
Proof state after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
hq : q > 1
h1 : v valp e.a1 ≥ 1
h2 : v valp e.a2 = 1
h3 : v valp e.a3 ≥ ↑q
h4 : v valp e.a4 ≥ ↑q + 1
h6 : v valp e.a6 ≥ 2 * ↑q
h2' : v valp (Model.b2 e.toModel) ≥ 1
⊢ v valp (Model.discr e.toModel) ≥ 2 * ↑q + 3
Theorem: ValidModel.v_discr_of_v_ai
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
hq : q > 1
h1 : v valp e.a1 ≥ 1
h2 : v valp e.a2 = 1
h3 : v valp e.a3 ≥ ↑q
h4 : v valp e.a4 ≥ ↑q + 1
h6 : v valp e.a6 ≥ 2 * ↑q
h2' : v valp (Model.b2 e.toModel) ≥ 1
⊢ v valp (Model.discr e.toModel) ≥ 2 * ↑q + 3
Tactic:
have h4' : valp e.b4 ≥ q + 1 := v_b4_of_v_a1_a3_a4 valp e h1 h3 h4
Proof state after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
hq : q > 1
h1 : v valp e.a1 ≥ 1
h2 : v valp e.a2 = 1
h3 : v valp e.a3 ≥ ↑q
h4 : v valp e.a4 ≥ ↑q + 1
h6 : v valp e.a6 ≥ 2 * ↑q
h2' : v valp (Model.b2 e.toModel) ≥ 1
h4' : v valp (Model.b4 e.toModel) ≥ ↑q + 1
⊢ v valp (Model.discr e.toModel) ≥ 2 * ↑q + 3
Theorem: ValidModel.v_discr_of_v_ai
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
hq : q > 1
h1 : v valp e.a1 ≥ 1
h2 : v valp e.a2 = 1
h3 : v valp e.a3 ≥ ↑q
h4 : v valp e.a4 ≥ ↑q + 1
h6 : v valp e.a6 ≥ 2 * ↑q
h2' : v valp (Model.b2 e.toModel) ≥ 1
h4' : v valp (Model.b4 e.toModel) ≥ ↑q + 1
⊢ v valp (Model.discr e.toModel) ≥ 2 * ↑q + 3
Tactic:
have h6' : valp e.b6 ≥ 2 * q := v_b6_of_v_a3_a6 valp e h3 h6
Proof state after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
hq : q > 1
h1 : v valp e.a1 ≥ 1
h2 : v valp e.a2 = 1
h3 : v valp e.a3 ≥ ↑q
h4 : v valp e.a4 ≥ ↑q + 1
h6 : v valp e.a6 ≥ 2 * ↑q
h2' : v valp (Model.b2 e.toModel) ≥ 1
h4' : v valp (Model.b4 e.toModel) ≥ ↑q + 1
h6' : v valp (Model.b6 e.toModel) ≥ 2 * ↑q
⊢ v valp (Model.discr e.toModel) ≥ 2 * ↑q + 3
Theorem: ValidModel.v_discr_of_v_ai
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
hq : q > 1
h1 : v valp e.a1 ≥ 1
h2 : v valp e.a2 = 1
h3 : v valp e.a3 ≥ ↑q
h4 : v valp e.a4 ≥ ↑q + 1
h6 : v valp e.a6 ≥ 2 * ↑q
h2' : v valp (Model.b2 e.toModel) ≥ 1
h4' : v valp (Model.b4 e.toModel) ≥ ↑q + 1
h6' : v valp (Model.b6 e.toModel) ≥ 2 * ↑q
⊢ v valp (Model.discr e.toModel) ≥ 2 * ↑q + 3
Tactic:
have h8' : valp e.b8 ≥ 2 * q + 1 := v_b8_of_v_ai valp e h1 h2 h3 h4 h6
Proof state after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
hq : q > 1
h1 : v valp e.a1 ≥ 1
h2 : v valp e.a2 = 1
h3 : v valp e.a3 ≥ ↑q
h4 : v valp e.a4 ≥ ↑q + 1
h6 : v valp e.a6 ≥ 2 * ↑q
h2' : v valp (Model.b2 e.toModel) ≥ 1
h4' : v valp (Model.b4 e.toModel) ≥ ↑q + 1
h6' : v valp (Model.b6 e.toModel) ≥ 2 * ↑q
h8' : v valp (Model.b8 e.toModel) ≥ 2 * ↑q + 1
⊢ v valp (Model.discr e.toModel) ≥ 2 * ↑q + 3
Theorem: ValidModel.v_discr_of_v_ai
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
hq : q > 1
h1 : v valp e.a1 ≥ 1
h2 : v valp e.a2 = 1
h3 : v valp e.a3 ≥ ↑q
h4 : v valp e.a4 ≥ ↑q + 1
h6 : v valp e.a6 ≥ 2 * ↑q
h2' : v valp (Model.b2 e.toModel) ≥ 1
h4' : v valp (Model.b4 e.toModel) ≥ ↑q + 1
h6' : v valp (Model.b6 e.toModel) ≥ 2 * ↑q
h8' : v valp (Model.b8 e.toModel) ≥ 2 * ↑q + 1
⊢ v valp (Model.discr e.toModel) ≥ 2 * ↑q + 3
Tactic:
apply_rules [val_add_ge_of_ge, val_sub_ge_of_ge] <;> . simp
  elinarith
Proof state after:
no goals
Theorem: ValidModel.v_discr_of_v_ai
Proof state before:
case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
hq : q > 1
h1 : v valp e.a1 ≥ 1
h2 : v valp e.a2 = 1
h3 : v valp e.a3 ≥ ↑q
h4 : v valp e.a4 ≥ ↑q + 1
h6 : v valp e.a6 ≥ 2 * ↑q
h2' : v valp (Model.b2 e.toModel) ≥ 1
h4' : v valp (Model.b4 e.toModel) ≥ ↑q + 1
h6' : v valp (Model.b6 e.toModel) ≥ 2 * ↑q
h8' : v valp (Model.b8 e.toModel) ≥ 2 * ↑q + 1
h2_symm : 1 = v valp e.a2
⊢ 2 * ↑q + 3 ≤ v valp (9 * Model.b2 e.toModel * Model.b4 e.toModel * Model.b6 e.toModel)
Tactic:
simp
Proof state after:
case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
hq : q > 1
h1 : v valp e.a1 ≥ 1
h2 : v valp e.a2 = 1
h3 : v valp e.a3 ≥ ↑q
h4 : v valp e.a4 ≥ ↑q + 1
h6 : v valp e.a6 ≥ 2 * ↑q
h2' : v valp (Model.b2 e.toModel) ≥ 1
h4' : v valp (Model.b4 e.toModel) ≥ ↑q + 1
h6' : v valp (Model.b6 e.toModel) ≥ 2 * ↑q
h8' : v valp (Model.b8 e.toModel) ≥ 2 * ↑q + 1
h2_symm : 1 = v valp e.a2
⊢ 2 * ↑q + 3 ≤ v valp 9 + v valp (Model.b2 e.toModel) + v valp (Model.b4 e.toModel) + v valp (Model.b6 e.toModel)
Theorem: ValidModel.v_discr_of_v_ai
Proof state before:
case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
hq : q > 1
h1 : v valp e.a1 ≥ 1
h2 : v valp e.a2 = 1
h3 : v valp e.a3 ≥ ↑q
h4 : v valp e.a4 ≥ ↑q + 1
h6 : v valp e.a6 ≥ 2 * ↑q
h2' : v valp (Model.b2 e.toModel) ≥ 1
h4' : v valp (Model.b4 e.toModel) ≥ ↑q + 1
h6' : v valp (Model.b6 e.toModel) ≥ 2 * ↑q
h8' : v valp (Model.b8 e.toModel) ≥ 2 * ↑q + 1
h2_symm : 1 = v valp e.a2
⊢ 2 * ↑q + 3 ≤ v valp 9 + v valp (Model.b2 e.toModel) + v valp (Model.b4 e.toModel) + v valp (Model.b6 e.toModel)
Tactic:
elinarith
Proof state after:
no goals
Theorem: ValidModel.small_char_div_12
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
hp : p = 2 ∨ p = 3
valp : SurjVal p
⊢ v valp 12 ≥ 1
Tactic:
cases hp with
| inl p2 =>
  rw [(show (12 : R) = 2 * 6 by norm_num)]
  apply val_mul_ge_of_left_ge
  rw [←p2]
  exact le_of_eq (valp.v_uniformizer).symm
| inr p3 =>
  rw [(show (12 : R) = 3 * 4 by norm_num)]
  apply val_mul_ge_of_left_ge
  rw [←p3]
  exact le_of_eq (valp.v_uniformizer).symm
Proof state after:
no goals
Theorem: ValidModel.small_char_div_12
Proof state before:
case inl
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p2 : p = 2
⊢ v valp 12 ≥ 1
Tactic:
rw [(show (12 : R) = 2 * 6 by norm_num)]
Proof state after:
case inl
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p2 : p = 2
⊢ v valp (2 * 6) ≥ 1
Theorem: ValidModel.small_char_div_12
Proof state before:
case inl
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p2 : p = 2
⊢ v valp (2 * 6) ≥ 1
Tactic:
apply val_mul_ge_of_left_ge
Proof state after:
case inl.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p2 : p = 2
⊢ 1 ≤ v valp 2