Theorem: Imo1968P2.prod_digits_le (Compfiles/Imo1968P2.lean)

State before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
⊢ (b.digits x).prod ≤ x
Tactic:
have h1 : Nat.digits b x ≠ [] :=
  Nat.digits_ne_nil_iff_ne_zero.mpr (Nat.pos_iff_ne_zero.mp xpos)
State after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
⊢ (b.digits x).prod ≤ x

State before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
⊢ (b.digits x).prod ≤ x
Tactic:
rw [←List.dropLast_append_getLast h1, List.prod_append, List.prod_singleton]
State after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x

State before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Tactic:
have h3 := Nat.ofDigits_digits b x
State after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 : Nat.ofDigits b (b.digits x) = x
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x

State before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 : Nat.ofDigits b (b.digits x) = x
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Tactic:
rw [Nat.ofDigits_eq_sum_mapIdx] at h3
State after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 : (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).sum = x
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x

State before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 : (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).sum = x
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Tactic:
have h4 : List.mapIdx (fun i a => a * b ^ i) (Nat.digits b x) ≠ [] :=
  List.mapIdx_eq_nil.not.mpr h1
State after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 : (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).sum = x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x

State before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 : (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).sum = x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Tactic:
rw [←List.dropLast_append_getLast (List.mapIdx_eq_nil.not.mpr h1),
    List.sum_append, List.sum_singleton] at h3
State after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x

State before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Tactic:
have h6 : List.getLast (List.mapIdx (fun i a => a * b ^ i) (Nat.digits b x)) h4 ≤ x :=
   by nth_rewrite 2 [←h3]; exact Nat.le_add_left _ _
State after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 ≤ x
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x

State before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 ≤ x
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Tactic:
have h7 : List.getLast (List.mapIdx (fun i a => a * b ^ i) (Nat.digits b x)) h4 =
     b ^ (List.dropLast (Nat.digits b x)).length * List.getLast (Nat.digits b x) h1 := by
  rw [lemma0 _ h1, mul_comm]
State after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 ≤ x
h7 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 =
    b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x

State before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 ≤ x
h7 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 =
    b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Tactic:
rw [h7] at h6
State after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1 ≤ x
h7 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 =
    b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x

State before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1 ≤ x
h7 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 =
    b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Tactic:
clear h7
State after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1 ≤ x
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x

State before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1 ≤ x
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Tactic:
have h8 : List.prod (List.dropLast (Nat.digits b x)) ≤
          b^(List.length (List.dropLast (Nat.digits b x))) := by
  have h10 : ∀ d ∈ List.dropLast (Nat.digits b x), d ≤ b := fun d hd ↦
    Nat.le_of_lt (Nat.digits_lt_base hb (List.mem_of_mem_dropLast hd))
  exact List.prod_le_pow_card (List.dropLast (Nat.digits b x)) b h10
State after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1 ≤ x
h8 : (b.digits x).dropLast.prod ≤ b ^ (b.digits x).dropLast.length
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x

State before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1 ≤ x
h8 : (b.digits x).dropLast.prod ≤ b ^ (b.digits x).dropLast.length
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Tactic:
calc _ ≤ _ := Nat.mul_le_mul_right _ h8
     _ ≤ _ := h6
State after:
no goals

State before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
⊢ (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 ≤ x
Tactic:
nth_rewrite 2 [←h3]
State after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
⊢ (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 ≤
    (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯

State before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
⊢ (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 ≤
    (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯
Tactic:
exact Nat.le_add_left _ _
State after:
no goals

State before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 ≤ x
⊢ (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 =
    b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1
Tactic:
rw [lemma0 _ h1, mul_comm]
State after:
no goals

State before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1 ≤ x
⊢ (b.digits x).dropLast.prod ≤ b ^ (b.digits x).dropLast.length
Tactic:
have h10 : ∀ d ∈ List.dropLast (Nat.digits b x), d ≤ b := fun d hd ↦
  Nat.le_of_lt (Nat.digits_lt_base hb (List.mem_of_mem_dropLast hd))
State after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1 ≤ x
h10 : ∀ d ∈ (b.digits x).dropLast, d ≤ b
⊢ (b.digits x).dropLast.prod ≤ b ^ (b.digits x).dropLast.length

State before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1 ≤ x
h10 : ∀ d ∈ (b.digits x).dropLast, d ≤ b
⊢ (b.digits x).dropLast.prod ≤ b ^ (b.digits x).dropLast.length
Tactic:
exact List.prod_le_pow_card (List.dropLast (Nat.digits b x)) b h10
State after:
no goals