internlm/Lean-Github huggingface dataset:
Theorem: Model.pi_scaling_of_b8
Proof state before:
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
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr 1 e.a1 * ENatValRing.sub_val evr 3 e.a3 * ENatValRing.sub_val evr 4 e.a4 +
          4 * ENatValRing.sub_val evr 2 e.a2 * ENatValRing.sub_val evr 6 e.a6 +
        ENatValRing.sub_val evr 2 e.a2 * ENatValRing.sub_val evr 3 e.a3 * ENatValRing.sub_val evr 3 e.a3 -
      ENatValRing.sub_val evr 4 e.a4 * ENatValRing.sub_val evr 4 e.a4
Tactic:
erw [←evr.sub_val_mul_right h3, ←evr.sub_val_mul_left h1, evr.sub_val_sub_val,
  ←evr.sub_val_mul_right h4, ←evr.sub_val_mul_left (val_mul_ge_of_both_ge evr.valtn h1 h3), evr.sub_val_sub_val]
Proof state after:
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
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr (Add.add 1 ↑3 + 4) (e.a1 * e.a3 * e.a4) +
          4 * ENatValRing.sub_val evr 2 e.a2 * ENatValRing.sub_val evr 6 e.a6 +
        ENatValRing.sub_val evr 2 e.a2 * ENatValRing.sub_val evr 3 e.a3 * ENatValRing.sub_val evr 3 e.a3 -
      ENatValRing.sub_val evr 4 e.a4 * ENatValRing.sub_val evr 4 e.a4
Theorem: Model.pi_scaling_of_b8
Proof state before:
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
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr (Add.add 1 ↑3 + 4) (e.a1 * e.a3 * e.a4) +
          4 * ENatValRing.sub_val evr 2 e.a2 * ENatValRing.sub_val evr 6 e.a6 +
        ENatValRing.sub_val evr 2 e.a2 * ENatValRing.sub_val evr 3 e.a3 * ENatValRing.sub_val evr 3 e.a3 -
      ENatValRing.sub_val evr 4 e.a4 * ENatValRing.sub_val evr 4 e.a4
Tactic:
rw [←evr.sub_val_mul_right h2, ←evr.sub_val_mul_right h6,
  ←evr.sub_val_mul_left (val_mul_ge_of_right_ge evr.valtn h2), evr.sub_val_sub_val]
Proof state after:
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
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr (Add.add 1 ↑3 + 4) (e.a1 * e.a3 * e.a4) +
          ENatValRing.sub_val evr (2 + 6) (4 * e.a2 * e.a6) +
        ENatValRing.sub_val evr 2 e.a2 * ENatValRing.sub_val evr 3 e.a3 * ENatValRing.sub_val evr 3 e.a3 -
      ENatValRing.sub_val evr 4 e.a4 * ENatValRing.sub_val evr 4 e.a4
Theorem: Model.pi_scaling_of_b8
Proof state before:
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
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr (Add.add 1 ↑3 + 4) (e.a1 * e.a3 * e.a4) +
          ENatValRing.sub_val evr (2 + 6) (4 * e.a2 * e.a6) +
        ENatValRing.sub_val evr 2 e.a2 * ENatValRing.sub_val evr 3 e.a3 * ENatValRing.sub_val evr 3 e.a3 -
      ENatValRing.sub_val evr 4 e.a4 * ENatValRing.sub_val evr 4 e.a4
Tactic:
erw [←evr.sub_val_mul_left h2, ←evr.sub_val_mul_right h3, ←evr.sub_val_mul_right h3,
  evr.sub_val_sub_val, ←evr.sub_val_mul_left (val_mul_ge_of_both_ge evr.valtn h2 h3), evr.sub_val_sub_val]
Proof state after:
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
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr (Add.add 1 ↑3 + 4) (e.a1 * e.a3 * e.a4) +
          ENatValRing.sub_val evr (2 + 6) (4 * e.a2 * e.a6) +
        ENatValRing.sub_val evr (Add.add ↑2 ↑3 + 3) (e.a2 * e.a3 * e.a3) -
      ENatValRing.sub_val evr 4 e.a4 * ENatValRing.sub_val evr 4 e.a4
Theorem: Model.pi_scaling_of_b8
Proof state before:
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
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr (Add.add 1 ↑3 + 4) (e.a1 * e.a3 * e.a4) +
          ENatValRing.sub_val evr (2 + 6) (4 * e.a2 * e.a6) +
        ENatValRing.sub_val evr (Add.add ↑2 ↑3 + 3) (e.a2 * e.a3 * e.a3) -
      ENatValRing.sub_val evr 4 e.a4 * ENatValRing.sub_val evr 4 e.a4
Tactic:
rw [←evr.sub_val_mul_right h4, ←evr.sub_val_mul_left h4, evr.sub_val_sub_val]
Proof state after:
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
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr (Add.add 1 ↑3 + 4) (e.a1 * e.a3 * e.a4) +
          ENatValRing.sub_val evr (2 + 6) (4 * e.a2 * e.a6) +
        ENatValRing.sub_val evr (Add.add ↑2 ↑3 + 3) (e.a2 * e.a3 * e.a3) -
      ENatValRing.sub_val evr (4 + 4) (e.a4 * e.a4)
Theorem: Model.pi_scaling_of_b8
Proof state before:
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
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr (Add.add 1 ↑3 + 4) (e.a1 * e.a3 * e.a4) +
          ENatValRing.sub_val evr (2 + 6) (4 * e.a2 * e.a6) +
        ENatValRing.sub_val evr (Add.add ↑2 ↑3 + 3) (e.a2 * e.a3 * e.a3) -
      ENatValRing.sub_val evr (4 + 4) (e.a4 * e.a4)
Tactic:
have h116 := val_mul_ge_of_both_ge evr.valtn (val_mul_ge_of_both_ge evr.valtn h1 h1) h6
Proof state after:
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
h116 : 1 + 1 + 6 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr (Add.add 1 ↑3 + 4) (e.a1 * e.a3 * e.a4) +
          ENatValRing.sub_val evr (2 + 6) (4 * e.a2 * e.a6) +
        ENatValRing.sub_val evr (Add.add ↑2 ↑3 + 3) (e.a2 * e.a3 * e.a3) -
      ENatValRing.sub_val evr (4 + 4) (e.a4 * e.a4)
Theorem: Model.pi_scaling_of_b8
Proof state before:
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
h116 : 1 + 1 + 6 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr (Add.add 1 ↑3 + 4) (e.a1 * e.a3 * e.a4) +
          ENatValRing.sub_val evr (2 + 6) (4 * e.a2 * e.a6) +
        ENatValRing.sub_val evr (Add.add ↑2 ↑3 + 3) (e.a2 * e.a3 * e.a3) -
      ENatValRing.sub_val evr (4 + 4) (e.a4 * e.a4)
Tactic:
have h134 := (val_mul_ge_of_both_ge evr.valtn (val_mul_ge_of_both_ge evr.valtn h1 h3) h4)
Proof state after:
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
h116 : 1 + 1 + 6 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
h134 : 1 + 3 + 4 ≤ v evr.valtn (e.a1 * e.a3 * e.a4)
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr (Add.add 1 ↑3 + 4) (e.a1 * e.a3 * e.a4) +
          ENatValRing.sub_val evr (2 + 6) (4 * e.a2 * e.a6) +
        ENatValRing.sub_val evr (Add.add ↑2 ↑3 + 3) (e.a2 * e.a3 * e.a3) -
      ENatValRing.sub_val evr (4 + 4) (e.a4 * e.a4)
Theorem: Model.pi_scaling_of_b8
Proof state before:
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
h116 : 1 + 1 + 6 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
h134 : 1 + 3 + 4 ≤ v evr.valtn (e.a1 * e.a3 * e.a4)
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr (Add.add 1 ↑3 + 4) (e.a1 * e.a3 * e.a4) +
          ENatValRing.sub_val evr (2 + 6) (4 * e.a2 * e.a6) +
        ENatValRing.sub_val evr (Add.add ↑2 ↑3 + 3) (e.a2 * e.a3 * e.a3) -
      ENatValRing.sub_val evr (4 + 4) (e.a4 * e.a4)
Tactic:
have h26 := val_mul_ge_of_both_ge evr.valtn (@val_mul_ge_of_right_ge R _ _ 2 p evr.valtn 4 e.a2 h2) h6
Proof state after:
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
h116 : 1 + 1 + 6 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
h134 : 1 + 3 + 4 ≤ v evr.valtn (e.a1 * e.a3 * e.a4)
h26 : 2 + 6 ≤ v evr.valtn (4 * e.a2 * e.a6)
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr (Add.add 1 ↑3 + 4) (e.a1 * e.a3 * e.a4) +
          ENatValRing.sub_val evr (2 + 6) (4 * e.a2 * e.a6) +
        ENatValRing.sub_val evr (Add.add ↑2 ↑3 + 3) (e.a2 * e.a3 * e.a3) -
      ENatValRing.sub_val evr (4 + 4) (e.a4 * e.a4)
Theorem: Model.pi_scaling_of_b8
Proof state before:
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
h116 : 1 + 1 + 6 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
h134 : 1 + 3 + 4 ≤ v evr.valtn (e.a1 * e.a3 * e.a4)
h26 : 2 + 6 ≤ v evr.valtn (4 * e.a2 * e.a6)
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr (Add.add 1 ↑3 + 4) (e.a1 * e.a3 * e.a4) +
          ENatValRing.sub_val evr (2 + 6) (4 * e.a2 * e.a6) +
        ENatValRing.sub_val evr (Add.add ↑2 ↑3 + 3) (e.a2 * e.a3 * e.a3) -
      ENatValRing.sub_val evr (4 + 4) (e.a4 * e.a4)
Tactic:
have h233 := val_mul_ge_of_both_ge evr.valtn (val_mul_ge_of_both_ge evr.valtn h2 h3) h3
Proof state after:
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
h116 : 1 + 1 + 6 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
h134 : 1 + 3 + 4 ≤ v evr.valtn (e.a1 * e.a3 * e.a4)
h26 : 2 + 6 ≤ v evr.valtn (4 * e.a2 * e.a6)
h233 : 2 + 3 + 3 ≤ v evr.valtn (e.a2 * e.a3 * e.a3)
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr (Add.add 1 ↑3 + 4) (e.a1 * e.a3 * e.a4) +
          ENatValRing.sub_val evr (2 + 6) (4 * e.a2 * e.a6) +
        ENatValRing.sub_val evr (Add.add ↑2 ↑3 + 3) (e.a2 * e.a3 * e.a3) -
      ENatValRing.sub_val evr (4 + 4) (e.a4 * e.a4)
Theorem: Model.pi_scaling_of_b8
Proof state before:
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
h116 : 1 + 1 + 6 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
h134 : 1 + 3 + 4 ≤ v evr.valtn (e.a1 * e.a3 * e.a4)
h26 : 2 + 6 ≤ v evr.valtn (4 * e.a2 * e.a6)
h233 : 2 + 3 + 3 ≤ v evr.valtn (e.a2 * e.a3 * e.a3)
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr (Add.add 1 ↑3 + 4) (e.a1 * e.a3 * e.a4) +
          ENatValRing.sub_val evr (2 + 6) (4 * e.a2 * e.a6) +
        ENatValRing.sub_val evr (Add.add ↑2 ↑3 + 3) (e.a2 * e.a3 * e.a3) -
      ENatValRing.sub_val evr (4 + 4) (e.a4 * e.a4)
Tactic:
have h44 := val_mul_ge_of_both_ge evr.valtn h4 h4
Proof state after:
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
h116 : 1 + 1 + 6 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
h134 : 1 + 3 + 4 ≤ v evr.valtn (e.a1 * e.a3 * e.a4)
h26 : 2 + 6 ≤ v evr.valtn (4 * e.a2 * e.a6)
h233 : 2 + 3 + 3 ≤ v evr.valtn (e.a2 * e.a3 * e.a3)
h44 : 4 + 4 ≤ v evr.valtn (e.a4 * e.a4)
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr (Add.add 1 ↑3 + 4) (e.a1 * e.a3 * e.a4) +
          ENatValRing.sub_val evr (2 + 6) (4 * e.a2 * e.a6) +
        ENatValRing.sub_val evr (Add.add ↑2 ↑3 + 3) (e.a2 * e.a3 * e.a3) -
      ENatValRing.sub_val evr (4 + 4) (e.a4 * e.a4)
Theorem: Model.pi_scaling_of_b8
Proof state before:
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
h116 : 1 + 1 + 6 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
h134 : 1 + 3 + 4 ≤ v evr.valtn (e.a1 * e.a3 * e.a4)
h26 : 2 + 6 ≤ v evr.valtn (4 * e.a2 * e.a6)
h233 : 2 + 3 + 3 ≤ v evr.valtn (e.a2 * e.a3 * e.a3)
h44 : 4 + 4 ≤ v evr.valtn (e.a4 * e.a4)
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr (Add.add 1 ↑3 + 4) (e.a1 * e.a3 * e.a4) +
          ENatValRing.sub_val evr (2 + 6) (4 * e.a2 * e.a6) +
        ENatValRing.sub_val evr (Add.add ↑2 ↑3 + 3) (e.a2 * e.a3 * e.a3) -
      ENatValRing.sub_val evr (4 + 4) (e.a4 * e.a4)
Tactic:
rw [←val_neg] at h134
Proof state after:
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
h116 : 1 + 1 + 6 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
h134 : 1 + 3 + 4 ≤ v evr.valtn (-(e.a1 * e.a3 * e.a4))
h26 : 2 + 6 ≤ v evr.valtn (4 * e.a2 * e.a6)
h233 : 2 + 3 + 3 ≤ v evr.valtn (e.a2 * e.a3 * e.a3)
h44 : 4 + 4 ≤ v evr.valtn (e.a4 * e.a4)
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr (Add.add 1 ↑3 + 4) (e.a1 * e.a3 * e.a4) +
          ENatValRing.sub_val evr (2 + 6) (4 * e.a2 * e.a6) +
        ENatValRing.sub_val evr (Add.add ↑2 ↑3 + 3) (e.a2 * e.a3 * e.a3) -
      ENatValRing.sub_val evr (4 + 4) (e.a4 * e.a4)
Theorem: Model.pi_scaling_of_b8
Proof state before:
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
h116 : 1 + 1 + 6 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
h134 : 1 + 3 + 4 ≤ v evr.valtn (-(e.a1 * e.a3 * e.a4))
h26 : 2 + 6 ≤ v evr.valtn (4 * e.a2 * e.a6)
h233 : 2 + 3 + 3 ≤ v evr.valtn (e.a2 * e.a3 * e.a3)
h44 : 4 + 4 ≤ v evr.valtn (e.a4 * e.a4)
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr (Add.add 1 ↑3 + 4) (e.a1 * e.a3 * e.a4) +
          ENatValRing.sub_val evr (2 + 6) (4 * e.a2 * e.a6) +
        ENatValRing.sub_val evr (Add.add ↑2 ↑3 + 3) (e.a2 * e.a3 * e.a3) -
      ENatValRing.sub_val evr (4 + 4) (e.a4 * e.a4)
Tactic:
rw [←val_neg] at h44
Proof state after:
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
h116 : 1 + 1 + 6 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
h134 : 1 + 3 + 4 ≤ v evr.valtn (-(e.a1 * e.a3 * e.a4))
h26 : 2 + 6 ≤ v evr.valtn (4 * e.a2 * e.a6)
h233 : 2 + 3 + 3 ≤ v evr.valtn (e.a2 * e.a3 * e.a3)
h44 : 4 + 4 ≤ v evr.valtn (-(e.a4 * e.a4))
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr (Add.add 1 ↑3 + 4) (e.a1 * e.a3 * e.a4) +
          ENatValRing.sub_val evr (2 + 6) (4 * e.a2 * e.a6) +
        ENatValRing.sub_val evr (Add.add ↑2 ↑3 + 3) (e.a2 * e.a3 * e.a3) -
      ENatValRing.sub_val evr (4 + 4) (e.a4 * e.a4)
Theorem: Model.pi_scaling_of_b8
Proof state before:
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
h116 : 1 + 1 + 6 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
h134 : 1 + 3 + 4 ≤ v evr.valtn (-(e.a1 * e.a3 * e.a4))
h26 : 2 + 6 ≤ v evr.valtn (4 * e.a2 * e.a6)
h233 : 2 + 3 + 3 ≤ v evr.valtn (e.a2 * e.a3 * e.a3)
h44 : 4 + 4 ≤ v evr.valtn (-(e.a4 * e.a4))
⊢ ↑(Add.add ↑4 ↑4) ≤ v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4) + 4 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3)

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
h116 : 1 + 1 + 6 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
h134 : 1 + 3 + 4 ≤ v evr.valtn (-(e.a1 * e.a3 * e.a4))
h26 : 2 + 6 ≤ v evr.valtn (4 * e.a2 * e.a6)
h233 : 2 + 3 + 3 ≤ v evr.valtn (e.a2 * e.a3 * e.a3)
h44 : 4 + 4 ≤ v evr.valtn (-(e.a4 * e.a4))
⊢ ↑(Add.add ((fun x x_1 => x + x_1) ↑2 ↑3) ↑3) ≤
    v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4) + 4 * e.a2 * e.a6)

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
h116 : 1 + 1 + 6 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
h134 : 1 + 3 + 4 ≤ v evr.valtn (-(e.a1 * e.a3 * e.a4))
h26 : 2 + 6 ≤ v evr.valtn (4 * e.a2 * e.a6)
h233 : 2 + 3 + 3 ≤ v evr.valtn (e.a2 * e.a3 * e.a3)
h44 : 4 + 4 ≤ v evr.valtn (-(e.a4 * e.a4))
⊢ ↑(Add.add ↑2 ↑6) ≤ v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4))
Tactic:
. exact val_add_ge_of_ge evr.valtn
    (val_add_ge_of_ge evr.valtn (val_add_ge_of_ge evr.valtn h116 h134) h26) h233
Proof state after:
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
h116 : 1 + 1 + 6 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
h134 : 1 + 3 + 4 ≤ v evr.valtn (-(e.a1 * e.a3 * e.a4))
h26 : 2 + 6 ≤ v evr.valtn (4 * e.a2 * e.a6)
h233 : 2 + 3 + 3 ≤ v evr.valtn (e.a2 * e.a3 * e.a3)
h44 : 4 + 4 ≤ v evr.valtn (-(e.a4 * e.a4))
⊢ ↑(Add.add ((fun x x_1 => x + x_1) ↑2 ↑3) ↑3) ≤
    v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4) + 4 * e.a2 * e.a6)

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
h116 : 1 + 1 + 6 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
h134 : 1 + 3 + 4 ≤ v evr.valtn (-(e.a1 * e.a3 * e.a4))
h26 : 2 + 6 ≤ v evr.valtn (4 * e.a2 * e.a6)
h233 : 2 + 3 + 3 ≤ v evr.valtn (e.a2 * e.a3 * e.a3)
h44 : 4 + 4 ≤ v evr.valtn (-(e.a4 * e.a4))
⊢ ↑(Add.add ↑2 ↑6) ≤ v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4))
Theorem: Model.pi_scaling_of_b8
Proof state before:
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
h116 : 1 + 1 + 6 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
h134 : 1 + 3 + 4 ≤ v evr.valtn (-(e.a1 * e.a3 * e.a4))
h26 : 2 + 6 ≤ v evr.valtn (4 * e.a2 * e.a6)
h233 : 2 + 3 + 3 ≤ v evr.valtn (e.a2 * e.a3 * e.a3)
h44 : 4 + 4 ≤ v evr.valtn (-(e.a4 * e.a4))
⊢ ↑(Add.add ((fun x x_1 => x + x_1) ↑2 ↑3) ↑3) ≤
    v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4) + 4 * e.a2 * e.a6)

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
h116 : 1 + 1 + 6 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
h134 : 1 + 3 + 4 ≤ v evr.valtn (-(e.a1 * e.a3 * e.a4))
h26 : 2 + 6 ≤ v evr.valtn (4 * e.a2 * e.a6)
h233 : 2 + 3 + 3 ≤ v evr.valtn (e.a2 * e.a3 * e.a3)
h44 : 4 + 4 ≤ v evr.valtn (-(e.a4 * e.a4))
⊢ ↑(Add.add ↑2 ↑6) ≤ v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4))
Tactic:
. exact val_add_ge_of_ge evr.valtn (val_add_ge_of_ge evr.valtn h116 h134) h26
Proof state after:
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
h116 : 1 + 1 + 6 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
h134 : 1 + 3 + 4 ≤ v evr.valtn (-(e.a1 * e.a3 * e.a4))
h26 : 2 + 6 ≤ v evr.valtn (4 * e.a2 * e.a6)
h233 : 2 + 3 + 3 ≤ v evr.valtn (e.a2 * e.a3 * e.a3)
h44 : 4 + 4 ≤ v evr.valtn (-(e.a4 * e.a4))
⊢ ↑(Add.add ↑2 ↑6) ≤ v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4))
Theorem: Model.pi_scaling_of_b8
Proof state before:
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
h116 : 1 + 1 + 6 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
h134 : 1 + 3 + 4 ≤ v evr.valtn (-(e.a1 * e.a3 * e.a4))
h26 : 2 + 6 ≤ v evr.valtn (4 * e.a2 * e.a6)
h233 : 2 + 3 + 3 ≤ v evr.valtn (e.a2 * e.a3 * e.a3)
h44 : 4 + 4 ≤ v evr.valtn (-(e.a4 * e.a4))
⊢ ↑(Add.add ↑2 ↑6) ≤ v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4))
Tactic:
. exact val_add_ge_of_ge evr.valtn h116 h134
Proof state after:
no goals
Theorem: Model.pi_scaling_of_b8
Proof state before:
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
h116 : 1 + 1 + 6 ≤ v evr.valtn (e.a1 * e.a1 * e.a6)
h134 : 1 + 3 + 4 ≤ v evr.valtn (-(e.a1 * e.a3 * e.a4))
h26 : 2 + 6 ≤ v evr.valtn (4 * e.a2 * e.a6)
h233 : 2 + 3 + 3 ≤ v evr.valtn (e.a2 * e.a3 * e.a3)
h44 : 4 + 4 ≤ v evr.valtn (-(e.a4 * e.a4))
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add ↑4 ↑4)
      (e.a1 * e.a1 * e.a6 - e.a1 * e.a3 * e.a4 + 4 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3 - e.a4 * e.a4)
Tactic:
rfl
Proof state after:
no goals