Theorem: HTPI.first_le_first (HTPILib/Chap7.lean)

State before:
p q : ℕ
l m : List ℕ
h1 : nondec_prime_list (p :: l)
h2 : nondec_prime_list (q :: m)
h3 : prod (p :: l) = prod (q :: m)
⊢ p ≤ q
Tactic:
define at h1
State after:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : nondec_prime_list (q :: m)
h3 : prod (p :: l) = prod (q :: m)
⊢ p ≤ q

State before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : nondec_prime_list (q :: m)
h3 : prod (p :: l) = prod (q :: m)
⊢ p ≤ q
Tactic:
define at h2
State after:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
⊢ p ≤ q

State before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
⊢ p ≤ q
Tactic:
have h4 : q ∣ prod (p :: l) := by
  define
  apply Exists.intro (prod m)
  rewrite [←prod_cons]
  show prod (p :: l) = prod (q :: m) from h3
  done
State after:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
⊢ p ≤ q

State before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
⊢ p ≤ q
Tactic:
have h5 : all_prime (q :: m) := h2.left
State after:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : all_prime (q :: m)
⊢ p ≤ q

State before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : all_prime (q :: m)
⊢ p ≤ q
Tactic:
rewrite [all_prime_cons] at h5
State after:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
⊢ p ≤ q

State before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
⊢ p ≤ q
Tactic:
have h6 : q ∈ p :: l := prime_in_list h5.left h1.left h4
State after:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h6 : q ∈ p :: l
⊢ p ≤ q

State before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h6 : q ∈ p :: l
⊢ p ≤ q
Tactic:
have h7 : nondec (p :: l) := h1.right
State after:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h6 : q ∈ p :: l
h7 : nondec (p :: l)
⊢ p ≤ q

State before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h6 : q ∈ p :: l
h7 : nondec (p :: l)
⊢ p ≤ q
Tactic:
rewrite [nondec_cons] at h7
State after:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h6 : q ∈ p :: l
h7 : (∀ m ∈ l, p ≤ m) ∧ nondec l
⊢ p ≤ q

State before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h6 : q ∈ p :: l
h7 : (∀ m ∈ l, p ≤ m) ∧ nondec l
⊢ p ≤ q
Tactic:
rewrite [List.mem_cons] at h6
State after:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h6 : q = p ∨ q ∈ l
h7 : (∀ m ∈ l, p ≤ m) ∧ nondec l
⊢ p ≤ q

State before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h6 : q = p ∨ q ∈ l
h7 : (∀ m ∈ l, p ≤ m) ∧ nondec l
⊢ p ≤ q
Tactic:
by_cases on h6
State after:
case Case_1
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h7 : (∀ m ∈ l, p ≤ m) ∧ nondec l
h6 : q = p
⊢ p ≤ q

case Case_2
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h7 : (∀ m ∈ l, p ≤ m) ∧ nondec l
h6 : q ∈ l
⊢ p ≤ q

State before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
⊢ q ∣ prod (p :: l)
Tactic:
define
State after:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
⊢ ∃ c, prod (p :: l) = q * c

State before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
⊢ ∃ c, prod (p :: l) = q * c
Tactic:
apply Exists.intro (prod m)
State after:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
⊢ prod (p :: l) = q * prod m

State before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
⊢ prod (p :: l) = q * prod m
Tactic:
rewrite [←prod_cons]
State after:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
⊢ prod (p :: l) = prod (q :: m)

State before:
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
⊢ prod (p :: l) = prod (q :: m)
Tactic:
show prod (p :: l) = prod (q :: m) from h3
State after:
no goals

State before:
case Case_1
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h7 : (∀ m ∈ l, p ≤ m) ∧ nondec l
h6 : q = p
⊢ p ≤ q
Tactic:
linarith
State after:
no goals

State before:
case Case_2
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h7 : (∀ m ∈ l, p ≤ m) ∧ nondec l
h6 : q ∈ l
⊢ p ≤ q
Tactic:
have h8 : ∀ m ∈ l, p ≤ m := h7.left
State after:
case Case_2
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h7 : (∀ m ∈ l, p ≤ m) ∧ nondec l
h6 : q ∈ l
h8 : ∀ m ∈ l, p ≤ m
⊢ p ≤ q

State before:
case Case_2
p q : ℕ
l m : List ℕ
h1 : all_prime (p :: l) ∧ nondec (p :: l)
h2 : all_prime (q :: m) ∧ nondec (q :: m)
h3 : prod (p :: l) = prod (q :: m)
h4 : q ∣ prod (p :: l)
h5 : prime q ∧ all_prime m
h7 : (∀ m ∈ l, p ≤ m) ∧ nondec l
h6 : q ∈ l
h8 : ∀ m ∈ l, p ≤ m
⊢ p ≤ q
Tactic:
show p ≤ q from h8 q h6
State after:
no goals